---

Step * of Lemma Wadd-Wzero

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero:A ⟶ 𝔹].
  ∀[z:W(A;a.B[a])]
    ∀[w1:W(A;a.B[a])]. (((w1 + z) = w1 ∈ W(A;a.B[a])) ∧ ((z + w1) = w1 ∈ W(A;a.B[a]))) supposing isZero(z) 
  supposing (∀a:A. (↑(zero a) ⇐⇒ ¬B[a])) ∧ (∀a1,a2:A.  ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A)))
BY
{ Auto }

1
1. A : Type
2. B : A ⟶ Type
3. zero : A ⟶ 𝔹
4. ∀a:A. (↑(zero a) ⇐⇒ ¬B[a])
5. ∀a1,a2:A.  ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A))
6. z : W(A;a.B[a])
7. isZero(z)
8. w1 : W(A;a.B[a])
⊢ (w1 + z) = w1 ∈ W(A;a.B[a])

2
1. A : Type
2. B : A ⟶ Type
3. zero : A ⟶ 𝔹
4. ∀a:A. (↑(zero a) ⇐⇒ ¬B[a])
5. ∀a1,a2:A.  ((↑(zero a1)) ⇒ (↑(zero a2)) ⇒ (a1 = a2 ∈ A))
6. z : W(A;a.B[a])
7. isZero(z)
8. w1 : W(A;a.B[a])
9. (w1 + z) = w1 ∈ W(A;a.B[a])
⊢ (z + w1) = w1 ∈ W(A;a.B[a])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[zero:A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[z:W(A;a.B[a])].  \mforall{}[w1:W(A;a.B[a])].  (((w1  +  z)  =  w1)  \mwedge{}  ((z  +  w1)  =  w1))  supposing  isZero(z) 
    supposing  (\mforall{}a:A.  (\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  \mneg{}B[a]))  \mwedge{}  (\mforall{}a1,a2:A.    ((\muparrow{}(zero  a1))  {}\mRightarrow{}  (\muparrow{}(zero  a2))  {}\mRightarrow{}  (a1  =  a2)))


By

---

Latex:
Auto

---

Home Index