### Nuprl Lemma : p-distrib

`∀[p:{2...}]. ∀[a,x,y:p-adics(p)].  ((a * x + y = a * x + a * y ∈ p-adics(p)) ∧ (x + y * a = x * a + y * a ∈ p-adics(p)))`

Proof

Definitions occuring in Statement :  p-mul: `x * y` p-add: `x + y` p-adics: `p-adics(p)` int_upper: `{i...}` uall: `∀[x:A]. B[x]` and: `P ∧ Q` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` crng: `CRng` rng: `Rng` p-adic-ring: `ℤ(p)` ring_p: `IsRing(T;plus;zero;neg;times;one)` rng_car: `|r|` pi1: `fst(t)` rng_plus: `+r` pi2: `snd(t)` rng_zero: `0` rng_minus: `-r` rng_times: `*` rng_one: `1` monoid_p: `IsMonoid(T;op;id)` group_p: `IsGroup(T;op;id;inv)` bilinear: `BiLinear(T;pl;tm)` ident: `Ident(T;op;id)` assoc: `Assoc(T;op)` inverse: `Inverse(T;op;id;inv)` infix_ap: `x f y` comm: `Comm(T;op)` and: `P ∧ Q`
Lemmas referenced :  p-adic-ring_wf crng_properties rng_properties int_upper_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename sqequalRule productElimination natural_numberEquality

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[a,x,y:p-adics(p)].    ((a  *  x  +  y  =  a  *  x  +  a  *  y)  \mwedge{}  (x  +  y  *  a  =  x  *  a  +  y  *  a))

Date html generated: 2018_05_21-PM-03_20_58
Last ObjectModification: 2018_05_19-AM-08_18_07

Theory : rings_1

Home Index