---

Step * of Lemma drng_all_properties

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

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

---

Latex:

---

Latex:
\mforall{}[r:DRng]
    (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;*)
    \mwedge{}  IsEqFun(|r|;=\msubb{}))


By

---

Latex:
D  0  THENM  (D  1)  THENA  Auto

---

Home Index