Step * 1 2 1 1 of Lemma rng_to_alg_wf


1. RngSig
2. IsRing(|R|;+R;0;-R;*;1)
3. Comm(|R|;*)
⊢ IsMonoid(|R|;*;1) ∧ BiLinear(|R|;+R;*) ∧ (∀a:|R|. Dist1op2opLR(|R|;* a;*))
BY
UnfoldTopAb THEN RepeatAndHD }

1
1. RngSig
2. IsGroup(|R|;+R;0;-R)
3. IsMonoid(|R|;*;1)
4. BiLinear(|R|;+R;*)
5. Comm(|R|;*)
⊢ IsMonoid(|R|;*;1) ∧ BiLinear(|R|;+R;*) ∧ (∀a:|R|. Dist1op2opLR(|R|;* a;*))


Latex:


Latex:

1.  R  :  RngSig
2.  IsRing(|R|;+R;0;-R;*;1)
3.  Comm(|R|;*)
\mvdash{}  IsMonoid(|R|;*;1)  \mwedge{}  BiLinear(|R|;+R;*)  \mwedge{}  (\mforall{}a:|R|.  Dist1op2opLR(|R|;*  a;*))


By


Latex:
UnfoldTopAb  2  THEN  RepeatAndHD  2




Home Index