---

Step * of Lemma rng_all_properties

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

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

---

Latex:

---

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


By

---

Latex:
D  0  THENM  (D  1)  THENA  Auto

---

Home Index