Proof of Theorem axi2m1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0r 11120 | . . . . . 6
⊢
0R ∈ R | 
| 2 |  | 1sr 11121 | . . . . . 6
⊢
1R ∈ R | 
| 3 |  | mulcnsr 11176 | . . . . . 6
⊢
(((0R ∈ R ∧
1R ∈ R) ∧
(0R ∈ R ∧
1R ∈ R)) →
(〈0R, 1R〉 ·
〈0R, 1R〉) =
〈((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))), ((1R
·R 0R)
+R (0R
·R
1R))〉) | 
| 4 | 1, 2, 1, 2, 3 | mp4an 693 | . . . . 5
⊢
(〈0R, 1R〉
· 〈0R, 1R〉)
= 〈((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))), ((1R
·R 0R)
+R (0R
·R
1R))〉 | 
| 5 |  | 00sr 11139 | . . . . . . . . 9
⊢
(0R ∈ R →
(0R ·R
0R) = 0R) | 
| 6 | 1, 5 | ax-mp 5 | . . . . . . . 8
⊢
(0R ·R
0R) = 0R | 
| 7 |  | 1idsr 11138 | . . . . . . . . . . 11
⊢
(1R ∈ R →
(1R ·R
1R) = 1R) | 
| 8 | 2, 7 | ax-mp 5 | . . . . . . . . . 10
⊢
(1R ·R
1R) = 1R | 
| 9 | 8 | oveq2i 7442 | . . . . . . . . 9
⊢
(-1R ·R
(1R ·R
1R)) = (-1R
·R
1R) | 
| 10 |  | m1r 11122 | . . . . . . . . . 10
⊢
-1R ∈ R | 
| 11 |  | 1idsr 11138 | . . . . . . . . . 10
⊢
(-1R ∈ R →
(-1R ·R
1R) = -1R) | 
| 12 | 10, 11 | ax-mp 5 | . . . . . . . . 9
⊢
(-1R ·R
1R) = -1R | 
| 13 | 9, 12 | eqtri 2765 | . . . . . . . 8
⊢
(-1R ·R
(1R ·R
1R)) = -1R | 
| 14 | 6, 13 | oveq12i 7443 | . . . . . . 7
⊢
((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))) = (0R
+R -1R) | 
| 15 |  | addcomsr 11127 | . . . . . . 7
⊢
(0R +R
-1R) = (-1R
+R 0R) | 
| 16 |  | 0idsr 11137 | . . . . . . . 8
⊢
(-1R ∈ R →
(-1R +R
0R) = -1R) | 
| 17 | 10, 16 | ax-mp 5 | . . . . . . 7
⊢
(-1R +R
0R) = -1R | 
| 18 | 14, 15, 17 | 3eqtri 2769 | . . . . . 6
⊢
((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))) = -1R | 
| 19 |  | 00sr 11139 | . . . . . . . . 9
⊢
(1R ∈ R →
(1R ·R
0R) = 0R) | 
| 20 | 2, 19 | ax-mp 5 | . . . . . . . 8
⊢
(1R ·R
0R) = 0R | 
| 21 |  | 1idsr 11138 | . . . . . . . . 9
⊢
(0R ∈ R →
(0R ·R
1R) = 0R) | 
| 22 | 1, 21 | ax-mp 5 | . . . . . . . 8
⊢
(0R ·R
1R) = 0R | 
| 23 | 20, 22 | oveq12i 7443 | . . . . . . 7
⊢
((1R ·R
0R) +R
(0R ·R
1R)) = (0R
+R 0R) | 
| 24 |  | 0idsr 11137 | . . . . . . . 8
⊢
(0R ∈ R →
(0R +R
0R) = 0R) | 
| 25 | 1, 24 | ax-mp 5 | . . . . . . 7
⊢
(0R +R
0R) = 0R | 
| 26 | 23, 25 | eqtri 2765 | . . . . . 6
⊢
((1R ·R
0R) +R
(0R ·R
1R)) = 0R | 
| 27 | 18, 26 | opeq12i 4878 | . . . . 5
⊢
〈((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))), ((1R
·R 0R)
+R (0R
·R 1R))〉 =
〈-1R,
0R〉 | 
| 28 | 4, 27 | eqtri 2765 | . . . 4
⊢
(〈0R, 1R〉
· 〈0R, 1R〉)
= 〈-1R,
0R〉 | 
| 29 | 28 | oveq1i 7441 | . . 3
⊢
((〈0R, 1R〉
· 〈0R, 1R〉)
+ 〈1R, 0R〉) =
(〈-1R, 0R〉 +
〈1R,
0R〉) | 
| 30 |  | addresr 11178 | . . . 4
⊢
((-1R ∈ R ∧
1R ∈ R) →
(〈-1R, 0R〉 +
〈1R, 0R〉) =
〈(-1R +R
1R),
0R〉) | 
| 31 | 10, 2, 30 | mp2an 692 | . . 3
⊢
(〈-1R, 0R〉 +
〈1R, 0R〉) =
〈(-1R +R
1R),
0R〉 | 
| 32 |  | m1p1sr 11132 | . . . 4
⊢
(-1R +R
1R) = 0R | 
| 33 | 32 | opeq1i 4876 | . . 3
⊢
〈(-1R +R
1R), 0R〉 =
〈0R,
0R〉 | 
| 34 | 29, 31, 33 | 3eqtri 2769 | . 2
⊢
((〈0R, 1R〉
· 〈0R, 1R〉)
+ 〈1R, 0R〉) =
〈0R,
0R〉 | 
| 35 |  | df-i 11164 | . . . 4
⊢ i =
〈0R,
1R〉 | 
| 36 | 35, 35 | oveq12i 7443 | . . 3
⊢ (i
· i) = (〈0R,
1R〉 · 〈0R,
1R〉) | 
| 37 |  | df-1 11163 | . . 3
⊢ 1 =
〈1R,
0R〉 | 
| 38 | 36, 37 | oveq12i 7443 | . 2
⊢ ((i
· i) + 1) = ((〈0R,
1R〉 · 〈0R,
1R〉) + 〈1R,
0R〉) | 
| 39 |  | df-0 11162 | . 2
⊢ 0 =
〈0R,
0R〉 | 
| 40 | 34, 38, 39 | 3eqtr4i 2775 | 1
⊢ ((i
· i) + 1) = 0 |