---

Step * of Lemma crng_all_properties

∀[r:CRng]
  (Assoc(|r|;+r)
  ∧ Ident(|r|;+r;0)
  ∧ Inverse(|r|;+r;0;-r)
  ∧ Assoc(|r|;*)
  ∧ Comm(|r|;*)
  ∧ Ident(|r|;*;1)
  ∧ BiLinear(|r|;+r;*))
BY
{ D 0 THENM (D 1) THENA Auto }

1
1. r : Rng
2. Comm(|r|;*)
⊢ Assoc(|r|;+r)
∧ Ident(|r|;+r;0)
∧ Inverse(|r|;+r;0;-r)
∧ Assoc(|r|;*)
∧ Comm(|r|;*)
∧ Ident(|r|;*;1)
∧ BiLinear(|r|;+r;*)

---

Latex:

---

Latex:
\mforall{}[r:CRng]
    (Assoc(|r|;+r)
    \mwedge{}  Ident(|r|;+r;0)
    \mwedge{}  Inverse(|r|;+r;0;-r)
    \mwedge{}  Assoc(|r|;*)
    \mwedge{}  Comm(|r|;*)
    \mwedge{}  Ident(|r|;*;1)
    \mwedge{}  BiLinear(|r|;+r;*))


By

---

Latex:
D  0  THENM  (D  1)  THENA  Auto

---

Home Index