---

Step * of Lemma nonzero-cross-imp_wf

∀[r:IntegDom{i}]. ∀[eq:∀x,y:|r|.  Dec(x = y ∈ |r|)]. ∀[a:{a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))} ]. ∀[b:{b:ℕ3 ⟶ |r|| 
                                                                                                      (¬(b
                                                                                                      = 0
                                                                                                      ∈ (ℕ3 ⟶ |r|)))
                                                                                                      ∧ (¬((a x b)
                                                                                                        = 0
                                                                                                        ∈ (ℕ3
                                                                                                          ⟶ |r|)))} ].
  (nonzero-cross-imp(r;eq;a;b) ∈ {l:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} | ((a . l) = 0 ∈ |r|) ∧ (¬((b . l) = 0 ∈ |r|))\000C} )
BY
{ (Auto THEN Fold `sq_exists` 0) }

1
1. r : IntegDom{i}
2. eq : ∀x,y:|r|.  Dec(x = y ∈ |r|)
3. a : {a:ℕ3 ⟶ |r|| ¬(a = 0 ∈ (ℕ3 ⟶ |r|))} 
4. b : {b:ℕ3 ⟶ |r|| (¬(b = 0 ∈ (ℕ3 ⟶ |r|))) ∧ (¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|)))} 
⊢ nonzero-cross-imp(r;eq;a;b) ∈ ∃l:∃p:ℕ3 ⟶ |r| [(¬(p = 0 ∈ (ℕ3 ⟶ |r|)))] [(((a . l) = 0 ∈ |r|)
                                                                           ∧ (¬((b . l) = 0 ∈ |r|)))]

---

Latex:

---

Latex:
\mforall{}[r:IntegDom\{i\}].  \mforall{}[eq:\mforall{}x,y:|r|.    Dec(x  =  y)].  \mforall{}[a:\{a:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(a  =  0)\}  ].  \mforall{}[b:\{b:\mBbbN{}3  {}\mrightarrow{}  |r|| 
                                                                                                                                                                    (\mneg{}(b  =  0))
                                                                                                                                                                    \mwedge{}  (\mneg{}((a  x  b)
                                                                                                                                                                        =  0))\}  ].
    (nonzero-cross-imp(r;eq;a;b)  \mmember{}  \{l:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  |  ((a  .  l)  =  0)  \mwedge{}  (\mneg{}((b  .  l)  =  0))\}  )


By

---

Latex:
(Auto  THEN  Fold  `sq\_exists`  0)

---

Home Index