Step
*
1
2
1
1
1
of Lemma
rng_to_alg_wf
1. R : 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;*))
BY
{ GenUnivCD THENM Try Trivial THENA Auto }
1
1. R : RngSig
2. IsGroup(|R|;+R;0;-R)
3. IsMonoid(|R|;*;1)
4. BiLinear(|R|;+R;*)
5. Comm(|R|;*)
6. a : |R|
⊢ Dist1op2opLR(|R|;* a;*)
Latex:
Latex:
1.  R  :  RngSig
2.  IsGroup(|R|;+R;0;-R)
3.  IsMonoid(|R|;*;1)
4.  BiLinear(|R|;+R;*)
5.  Comm(|R|;*)
\mvdash{}  IsMonoid(|R|;*;1)  \mwedge{}  BiLinear(|R|;+R;*)  \mwedge{}  (\mforall{}a:|R|.  Dist1op2opLR(|R|;*  a;*))
By
Latex:
GenUnivCD  THENM  Try  Trivial  THENA  Auto
Home
Index