---

Step * 1 1 6 1 1 1 1 of Lemma rng-pps_wf


1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
4. a : ℕ3 ⟶ |r|@i
5. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
6. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
7. b : ℕ3 ⟶ |r|@i
8. ¬(b = 0 ∈ (ℕ3 ⟶ |r|))
9. p : ℕ3 ⟶ |r|@i
10. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
11. (p . a) = 0 ∈ |r|
12. _2 : (¬((p . a) = 0 ∈ |r|)) ⟶ False
13. _3 : ((p . b) = 0 ∈ |r|) ⟶ False
14. c1 : |r|
15. c2 : |r|
16. ¬(c1 = 0 ∈ |r|)
17. ¬(c2 = 0 ∈ |r|)
18. (c1*a) = (c2*b) ∈ (ℕ3 ⟶ |r|)
19. ∀x,y:|r|.  Dec(x = y ∈ |r|)
20. (p . (c1*a)) = (p . (c2*b)) ∈ |r|
⊢ (p . b) = 0 ∈ |r|
BY
{ ((RWO "scalar-product-comm" (-1) THENA Auto)
   THEN (RWO "scalar-product-comm" 0 THENA Auto)
   THEN (RWO "scalar-product-comm" 11 THENA Auto)) }

1
1. r : IntegDom{i}@i'
2. eq : EqDecider(|r|)
3. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
4. a : ℕ3 ⟶ |r|@i
5. ¬(a = 0 ∈ (ℕ3 ⟶ |r|))
6. ∀p:ℕ3 ⟶ |r|. (¬(p = 0 ∈ (ℕ3 ⟶ |r|)) ∈ 𝕌{[1 | i 0]})
7. b : ℕ3 ⟶ |r|@i
8. ¬(b = 0 ∈ (ℕ3 ⟶ |r|))
9. p : ℕ3 ⟶ |r|@i
10. ¬(p = 0 ∈ (ℕ3 ⟶ |r|))
11. (a . p) = 0 ∈ |r|
12. _2 : (¬((p . a) = 0 ∈ |r|)) ⟶ False
13. _3 : ((p . b) = 0 ∈ |r|) ⟶ False
14. c1 : |r|
15. c2 : |r|
16. ¬(c1 = 0 ∈ |r|)
17. ¬(c2 = 0 ∈ |r|)
18. (c1*a) = (c2*b) ∈ (ℕ3 ⟶ |r|)
19. ∀x,y:|r|.  Dec(x = y ∈ |r|)
20. ((c1*a) . p) = ((c2*b) . p) ∈ |r|
⊢ (b . p) = 0 ∈ |r|

---

Latex:

---

Latex:

1.  r  :  IntegDom\{i\}@i'
2.  eq  :  EqDecider(|r|)
3.  \mforall{}p:\mBbbN{}3  {}\mrightarrow{}  |r|.  (\mneg{}(p  =  0)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
4.  a  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
5.  \mneg{}(a  =  0)
6.  \mforall{}p:\mBbbN{}3  {}\mrightarrow{}  |r|.  (\mneg{}(p  =  0)  \mmember{}  \mBbbU{}\{[1  |  i  0]\})
7.  b  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
8.  \mneg{}(b  =  0)
9.  p  :  \mBbbN{}3  {}\mrightarrow{}  |r|@i
10.  \mneg{}(p  =  0)
11.  (p  .  a)  =  0
12.  $_{2}$  :  (\mneg{}((p  .  a)  =  0))  {}\mrightarrow{}  False
13.  $_{3}$  :  ((p  .  b)  =  0)  {}\mrightarrow{}  False
14.  c1  :  |r|
15.  c2  :  |r|
16.  \mneg{}(c1  =  0)
17.  \mneg{}(c2  =  0)
18.  (c1*a)  =  (c2*b)
19.  \mforall{}x,y:|r|.    Dec(x  =  y)
20.  (p  .  (c1*a))  =  (p  .  (c2*b))
\mvdash{}  (p  .  b)  =  0


By

---

Latex:
((RWO  "scalar-product-comm"  (-1)  THENA  Auto)
  THEN  (RWO  "scalar-product-comm"  0  THENA  Auto)
  THEN  (RWO  "scalar-product-comm"  11  THENA  Auto))

---

Home Index