---

Step * of Lemma rng-pp-nontrivial-4

∀r:IntegDom{i}. ∀eq:EqDecider(|r|). ∀p:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} .
  ∃l,m,n:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
   ((¬¬((p . l) = 0 ∈ |r|))
   ∧ (¬¬((p . m) = 0 ∈ |r|))
   ∧ (¬¬((p . n) = 0 ∈ |r|))
   ∧ (∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . l) = 0 ∈ |r|)) ∧ (¬((a . m) = 0 ∈ |r|))))
   ∧ (∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . m) = 0 ∈ |r|)) ∧ (¬((a . n) = 0 ∈ |r|))))
   ∧ (∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . n) = 0 ∈ |r|)) ∧ (¬((a . l) = 0 ∈ |r|)))))
BY
{ (Auto
   THEN (InstLemma `deq-implies` [⌜|r|⌝]⋅ THENA Auto)
   THEN (InstLemma `rng-pp-nontrivial-2` [⌜r⌝;⌜p⌝]⋅ THENA Auto)
   THEN RepeatFor 4 (ParallelLast)
   THEN RepeatFor 3 ((ParallelLast
                     ORELSE ((RemoveDoubleNegation THENA Auto) THEN RWO "scalar-product-comm" 0 THEN Auto)
                     ))
   THEN Try (ParallelLast)
   THEN skip{(Try (((FLemma `cross-product-non-zero-implies` [-1] THENA Auto) THEN ParallelLast THEN Auto))
              THEN (RemoveDoubleNegation THENA Auto)
              THEN RWO "scalar-product-comm" 0
              THEN Auto)}) }

1
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
7. c : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
8. (a . p) = 0 ∈ |r|
9. (b . p) = 0 ∈ |r|
10. (c . p) = 0 ∈ |r|
11. (¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))) ∧ (¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|)))
12. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃a@0:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a@0 . a) = 0 ∈ |r|)) ∧ (¬((a@0 . b) = 0 ∈ |r|)))

2
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
7. c : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
8. (a . p) = 0 ∈ |r|
9. (b . p) = 0 ∈ |r|
10. (c . p) = 0 ∈ |r|
11. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
12. ¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))
13. ¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃a:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a . b) = 0 ∈ |r|)) ∧ (¬((a . c) = 0 ∈ |r|)))

3
1. r : IntegDom{i}
2. eq : EqDecider(|r|)
3. p : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
4. ∀x,y:|r|.  Dec(x = y ∈ |r|)
5. a : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
6. b : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
7. c : {p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} 
8. (a . p) = 0 ∈ |r|
9. (b . p) = 0 ∈ |r|
10. (c . p) = 0 ∈ |r|
11. ¬((a x b) = 0 ∈ (ℕ3 ⟶ |r|))
12. ¬((b x c) = 0 ∈ (ℕ3 ⟶ |r|))
13. ¬((c x a) = 0 ∈ (ℕ3 ⟶ |r|))
⊢ ∃a@0:{p:ℕ3 ⟶ |r|| ¬(p = 0 ∈ (ℕ3 ⟶ |r|))} . ((¬¬((a@0 . c) = 0 ∈ |r|)) ∧ (¬((a@0 . a) = 0 ∈ |r|)))

---

Latex:

---

Latex:
\mforall{}r:IntegDom\{i\}.  \mforall{}eq:EqDecider(|r|).  \mforall{}p:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .
    \mexists{}l,m,n:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\} 
      ((\mneg{}\mneg{}((p  .  l)  =  0))
      \mwedge{}  (\mneg{}\mneg{}((p  .  m)  =  0))
      \mwedge{}  (\mneg{}\mneg{}((p  .  n)  =  0))
      \mwedge{}  (\mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  l)  =  0))  \mwedge{}  (\mneg{}((a  .  m)  =  0))))
      \mwedge{}  (\mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  m)  =  0))  \mwedge{}  (\mneg{}((a  .  n)  =  0))))
      \mwedge{}  (\mexists{}a:\{p:\mBbbN{}3  {}\mrightarrow{}  |r||  \mneg{}(p  =  0)\}  .  ((\mneg{}\mneg{}((a  .  n)  =  0))  \mwedge{}  (\mneg{}((a  .  l)  =  0)))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `deq-implies`  [\mkleeneopen{}|r|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rng-pp-nontrivial-2`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  4  (ParallelLast)
  THEN  RepeatFor  3  ((ParallelLast
                                      ORELSE  ((RemoveDoubleNegation  THENA  Auto)
                                                      THEN  RWO  "scalar-product-comm"  0
                                                      THEN  Auto)
                                      ))
  THEN  Try  (ParallelLast)
  THEN  skip\{(Try  (((FLemma  `cross-product-non-zero-implies`  [-1]  THENA  Auto)
                                    THEN  ParallelLast
                                    THEN  Auto))
                        THEN  (RemoveDoubleNegation  THENA  Auto)
                        THEN  RWO  "scalar-product-comm"  0
                        THEN  Auto)\})

---

Home Index