Step | Hyp | Ref
| Expression |
1 | | 0r 7748 |
. . . . . 6
⊢
0R ∈ R |
2 | | 1sr 7749 |
. . . . . 6
⊢
1R ∈ R |
3 | | mulcnsr 7833 |
. . . . . 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 7767 |
. . . . . . . . 9
⊢
(0R ∈ R →
(0R ·R
0R) = 0R) |
6 | 1, 5 | ax-mp 5 |
. . . . . . . 8
⊢
(0R ·R
0R) = 0R |
7 | | 1idsr 7766 |
. . . . . . . . . . 11
⊢
(1R ∈ R →
(1R ·R
1R) = 1R) |
8 | 2, 7 | ax-mp 5 |
. . . . . . . . . 10
⊢
(1R ·R
1R) = 1R |
9 | 8 | oveq2i 5885 |
. . . . . . . . 9
⊢
(-1R ·R
(1R ·R
1R)) = (-1R
·R
1R) |
10 | | m1r 7750 |
. . . . . . . . . 10
⊢
-1R ∈ R |
11 | | 1idsr 7766 |
. . . . . . . . . 10
⊢
(-1R ∈ R →
(-1R ·R
1R) = -1R) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢
(-1R ·R
1R) = -1R |
13 | 9, 12 | eqtri 2198 |
. . . . . . . 8
⊢
(-1R ·R
(1R ·R
1R)) = -1R |
14 | 6, 13 | oveq12i 5886 |
. . . . . . 7
⊢
((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))) = (0R
+R -1R) |
15 | | addcomsrg 7753 |
. . . . . . . 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 7765 |
. . . . . . . 8
⊢
(-1R ∈ R →
(-1R +R
0R) = -1R) |
18 | 10, 17 | ax-mp 5 |
. . . . . . 7
⊢
(-1R +R
0R) = -1R |
19 | 14, 16, 18 | 3eqtri 2202 |
. . . . . 6
⊢
((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))) = -1R |
20 | | 00sr 7767 |
. . . . . . . . 9
⊢
(1R ∈ R →
(1R ·R
0R) = 0R) |
21 | 2, 20 | ax-mp 5 |
. . . . . . . 8
⊢
(1R ·R
0R) = 0R |
22 | | 1idsr 7766 |
. . . . . . . . 9
⊢
(0R ∈ R →
(0R ·R
1R) = 0R) |
23 | 1, 22 | ax-mp 5 |
. . . . . . . 8
⊢
(0R ·R
1R) = 0R |
24 | 21, 23 | oveq12i 5886 |
. . . . . . 7
⊢
((1R ·R
0R) +R
(0R ·R
1R)) = (0R
+R 0R) |
25 | | 0idsr 7765 |
. . . . . . . 8
⊢
(0R ∈ R →
(0R +R
0R) = 0R) |
26 | 1, 25 | ax-mp 5 |
. . . . . . 7
⊢
(0R +R
0R) = 0R |
27 | 24, 26 | eqtri 2198 |
. . . . . 6
⊢
((1R ·R
0R) +R
(0R ·R
1R)) = 0R |
28 | 19, 27 | opeq12i 3783 |
. . . . 5
⊢
⟨((0R ·R
0R) +R
(-1R ·R
(1R ·R
1R))), ((1R
·R 0R)
+R (0R
·R 1R))⟩ =
⟨-1R,
0R⟩ |
29 | 4, 28 | eqtri 2198 |
. . . 4
⊢
(⟨0R, 1R⟩
· ⟨0R, 1R⟩)
= ⟨-1R,
0R⟩ |
30 | 29 | oveq1i 5884 |
. . 3
⊢
((⟨0R, 1R⟩
· ⟨0R, 1R⟩)
+ ⟨1R, 0R⟩) =
(⟨-1R, 0R⟩ +
⟨1R,
0R⟩) |
31 | | addresr 7835 |
. . . 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 7758 |
. . . 4
⊢
(-1R +R
1R) = 0R |
34 | 33 | opeq1i 3781 |
. . 3
⊢
⟨(-1R +R
1R), 0R⟩ =
⟨0R,
0R⟩ |
35 | 30, 32, 34 | 3eqtri 2202 |
. 2
⊢
((⟨0R, 1R⟩
· ⟨0R, 1R⟩)
+ ⟨1R, 0R⟩) =
⟨0R,
0R⟩ |
36 | | df-i 7819 |
. . . 4
⊢ i =
⟨0R,
1R⟩ |
37 | 36, 36 | oveq12i 5886 |
. . 3
⊢ (i
· i) = (⟨0R,
1R⟩ · ⟨0R,
1R⟩) |
38 | | df-1 7818 |
. . 3
⊢ 1 =
⟨1R,
0R⟩ |
39 | 37, 38 | oveq12i 5886 |
. 2
⊢ ((i
· i) + 1) = ((⟨0R,
1R⟩ · ⟨0R,
1R⟩) + ⟨1R,
0R⟩) |
40 | | df-0 7817 |
. 2
⊢ 0 =
⟨0R,
0R⟩ |
41 | 35, 39, 40 | 3eqtr4i 2208 |
1
⊢ ((i
· i) + 1) = 0 |