Proof of Theorem axi2m1
| Step | Hyp | Ref
| Expression |
| 1 | | 0r 7817 |
. . . . . 6
⊢
0R ∈ R |
| 2 | | 1sr 7818 |
. . . . . 6
⊢
1R ∈ R |
| 3 | | mulcnsr 7902 |
. . . . . 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 427 |
. . . . 5
⊢
(〈0R, 1R〉
· 〈0R, 1R〉)
= 〈((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))), ((1R
·R 0R)
+R (0R
·R
1R))〉 |
| 5 | | 00sr 7836 |
. . . . . . . . 9
⊢
(0R ∈ R →
(0R ·R
0R) = 0R) |
| 6 | 1, 5 | ax-mp 5 |
. . . . . . . 8
⊢
(0R ·R
0R) = 0R |
| 7 | | 1idsr 7835 |
. . . . . . . . . . 11
⊢
(1R ∈ R →
(1R ·R
1R) = 1R) |
| 8 | 2, 7 | ax-mp 5 |
. . . . . . . . . 10
⊢
(1R ·R
1R) = 1R |
| 9 | 8 | oveq2i 5933 |
. . . . . . . . 9
⊢
(-1R ·R
(1R ·R
1R)) = (-1R
·R
1R) |
| 10 | | m1r 7819 |
. . . . . . . . . 10
⊢
-1R ∈ R |
| 11 | | 1idsr 7835 |
. . . . . . . . . 10
⊢
(-1R ∈ R →
(-1R ·R
1R) = -1R) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1R ·R
1R) = -1R |
| 13 | 9, 12 | eqtri 2217 |
. . . . . . . 8
⊢
(-1R ·R
(1R ·R
1R)) = -1R |
| 14 | 6, 13 | oveq12i 5934 |
. . . . . . 7
⊢
((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))) = (0R
+R -1R) |
| 15 | | addcomsrg 7822 |
. . . . . . . 8
⊢
((0R ∈ R ∧
-1R ∈ R) →
(0R +R
-1R) = (-1R
+R 0R)) |
| 16 | 1, 10, 15 | mp2an 426 |
. . . . . . 7
⊢
(0R +R
-1R) = (-1R
+R 0R) |
| 17 | | 0idsr 7834 |
. . . . . . . 8
⊢
(-1R ∈ R →
(-1R +R
0R) = -1R) |
| 18 | 10, 17 | ax-mp 5 |
. . . . . . 7
⊢
(-1R +R
0R) = -1R |
| 19 | 14, 16, 18 | 3eqtri 2221 |
. . . . . 6
⊢
((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))) = -1R |
| 20 | | 00sr 7836 |
. . . . . . . . 9
⊢
(1R ∈ R →
(1R ·R
0R) = 0R) |
| 21 | 2, 20 | ax-mp 5 |
. . . . . . . 8
⊢
(1R ·R
0R) = 0R |
| 22 | | 1idsr 7835 |
. . . . . . . . 9
⊢
(0R ∈ R →
(0R ·R
1R) = 0R) |
| 23 | 1, 22 | ax-mp 5 |
. . . . . . . 8
⊢
(0R ·R
1R) = 0R |
| 24 | 21, 23 | oveq12i 5934 |
. . . . . . 7
⊢
((1R ·R
0R) +R
(0R ·R
1R)) = (0R
+R 0R) |
| 25 | | 0idsr 7834 |
. . . . . . . 8
⊢
(0R ∈ R →
(0R +R
0R) = 0R) |
| 26 | 1, 25 | ax-mp 5 |
. . . . . . 7
⊢
(0R +R
0R) = 0R |
| 27 | 24, 26 | eqtri 2217 |
. . . . . 6
⊢
((1R ·R
0R) +R
(0R ·R
1R)) = 0R |
| 28 | 19, 27 | opeq12i 3813 |
. . . . 5
⊢
〈((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))), ((1R
·R 0R)
+R (0R
·R 1R))〉 =
〈-1R,
0R〉 |
| 29 | 4, 28 | eqtri 2217 |
. . . 4
⊢
(〈0R, 1R〉
· 〈0R, 1R〉)
= 〈-1R,
0R〉 |
| 30 | 29 | oveq1i 5932 |
. . 3
⊢
((〈0R, 1R〉
· 〈0R, 1R〉)
+ 〈1R, 0R〉) =
(〈-1R, 0R〉 +
〈1R,
0R〉) |
| 31 | | addresr 7904 |
. . . 4
⊢
((-1R ∈ R ∧
1R ∈ R) →
(〈-1R, 0R〉 +
〈1R, 0R〉) =
〈(-1R +R
1R),
0R〉) |
| 32 | 10, 2, 31 | mp2an 426 |
. . 3
⊢
(〈-1R, 0R〉 +
〈1R, 0R〉) =
〈(-1R +R
1R),
0R〉 |
| 33 | | m1p1sr 7827 |
. . . 4
⊢
(-1R +R
1R) = 0R |
| 34 | 33 | opeq1i 3811 |
. . 3
⊢
〈(-1R +R
1R), 0R〉 =
〈0R,
0R〉 |
| 35 | 30, 32, 34 | 3eqtri 2221 |
. 2
⊢
((〈0R, 1R〉
· 〈0R, 1R〉)
+ 〈1R, 0R〉) =
〈0R,
0R〉 |
| 36 | | df-i 7888 |
. . . 4
⊢ i =
〈0R,
1R〉 |
| 37 | 36, 36 | oveq12i 5934 |
. . 3
⊢ (i
· i) = (〈0R,
1R〉 · 〈0R,
1R〉) |
| 38 | | df-1 7887 |
. . 3
⊢ 1 =
〈1R,
0R〉 |
| 39 | 37, 38 | oveq12i 5934 |
. 2
⊢ ((i
· i) + 1) = ((〈0R,
1R〉 · 〈0R,
1R〉) + 〈1R,
0R〉) |
| 40 | | df-0 7886 |
. 2
⊢ 0 =
〈0R,
0R〉 |
| 41 | 35, 39, 40 | 3eqtr4i 2227 |
1
⊢ ((i
· i) + 1) = 0 |