Step | Hyp | Ref
| Expression |
1 | | df-m1r 11057 |
. . 3
⊢
-1R = [⟨1P,
(1P +P
1P)⟩]
~R |
2 | 1, 1 | oveq12i 7421 |
. 2
⊢
(-1R ·R
-1R) = ([⟨1P,
(1P +P
1P)⟩] ~R
·R [⟨1P,
(1P +P
1P)⟩] ~R
) |
3 | | df-1r 11056 |
. . 3
⊢
1R = [⟨(1P
+P 1P),
1P⟩] ~R |
4 | | 1pr 11010 |
. . . . 5
⊢
1P ∈ P |
5 | | addclpr 11013 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
6 | 4, 4, 5 | mp2an 691 |
. . . . 5
⊢
(1P +P
1P) ∈ P |
7 | | mulsrpr 11071 |
. . . . 5
⊢
(((1P ∈ P ∧
(1P +P
1P) ∈ P) ∧
(1P ∈ P ∧
(1P +P
1P) ∈ P)) →
([⟨1P, (1P
+P 1P)⟩]
~R ·R
[⟨1P, (1P
+P 1P)⟩]
~R ) = [⟨((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P))),
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))⟩] ~R
) |
8 | 4, 6, 4, 6, 7 | mp4an 692 |
. . . 4
⊢
([⟨1P, (1P
+P 1P)⟩]
~R ·R
[⟨1P, (1P
+P 1P)⟩]
~R ) = [⟨((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P))),
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))⟩]
~R |
9 | | addasspr 11017 |
. . . . . 6
⊢
((1P +P
1P) +P
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))) = (1P
+P (1P
+P ((1P
·P (1P
+P 1P))
+P ((1P
+P 1P)
·P
1P)))) |
10 | | 1idpr 11024 |
. . . . . . . . 9
⊢
(1P ∈ P →
(1P ·P
1P) = 1P) |
11 | 4, 10 | ax-mp 5 |
. . . . . . . 8
⊢
(1P ·P
1P) = 1P |
12 | | distrpr 11023 |
. . . . . . . . 9
⊢
((1P +P
1P) ·P
(1P +P
1P)) = (((1P
+P 1P)
·P 1P)
+P ((1P
+P 1P)
·P
1P)) |
13 | | mulcompr 11018 |
. . . . . . . . . 10
⊢
(1P ·P
(1P +P
1P)) = ((1P
+P 1P)
·P
1P) |
14 | 13 | oveq1i 7419 |
. . . . . . . . 9
⊢
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P)) = (((1P
+P 1P)
·P 1P)
+P ((1P
+P 1P)
·P
1P)) |
15 | 12, 14 | eqtr4i 2764 |
. . . . . . . 8
⊢
((1P +P
1P) ·P
(1P +P
1P)) = ((1P
·P (1P
+P 1P))
+P ((1P
+P 1P)
·P
1P)) |
16 | 11, 15 | oveq12i 7421 |
. . . . . . 7
⊢
((1P ·P
1P) +P
((1P +P
1P) ·P
(1P +P
1P))) = (1P
+P ((1P
·P (1P
+P 1P))
+P ((1P
+P 1P)
·P
1P))) |
17 | 16 | oveq2i 7420 |
. . . . . 6
⊢
(1P +P
((1P ·P
1P) +P
((1P +P
1P) ·P
(1P +P
1P)))) = (1P
+P (1P
+P ((1P
·P (1P
+P 1P))
+P ((1P
+P 1P)
·P
1P)))) |
18 | 9, 17 | eqtr4i 2764 |
. . . . 5
⊢
((1P +P
1P) +P
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))) = (1P
+P ((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P)))) |
19 | | mulclpr 11015 |
. . . . . . . 8
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P ·P
1P) ∈ P) |
20 | 4, 4, 19 | mp2an 691 |
. . . . . . 7
⊢
(1P ·P
1P) ∈ P |
21 | | mulclpr 11015 |
. . . . . . . 8
⊢
(((1P +P
1P) ∈ P ∧
(1P +P
1P) ∈ P) →
((1P +P
1P) ·P
(1P +P
1P)) ∈ P) |
22 | 6, 6, 21 | mp2an 691 |
. . . . . . 7
⊢
((1P +P
1P) ·P
(1P +P
1P)) ∈ P |
23 | | addclpr 11013 |
. . . . . . 7
⊢
(((1P ·P
1P) ∈ P ∧
((1P +P
1P) ·P
(1P +P
1P)) ∈ P) →
((1P ·P
1P) +P
((1P +P
1P) ·P
(1P +P
1P))) ∈ P) |
24 | 20, 22, 23 | mp2an 691 |
. . . . . 6
⊢
((1P ·P
1P) +P
((1P +P
1P) ·P
(1P +P
1P))) ∈ P |
25 | | mulclpr 11015 |
. . . . . . . 8
⊢
((1P ∈ P ∧
(1P +P
1P) ∈ P) →
(1P ·P
(1P +P
1P)) ∈ P) |
26 | 4, 6, 25 | mp2an 691 |
. . . . . . 7
⊢
(1P ·P
(1P +P
1P)) ∈ P |
27 | | mulclpr 11015 |
. . . . . . . 8
⊢
(((1P +P
1P) ∈ P ∧
1P ∈ P) →
((1P +P
1P) ·P
1P) ∈ P) |
28 | 6, 4, 27 | mp2an 691 |
. . . . . . 7
⊢
((1P +P
1P) ·P
1P) ∈ P |
29 | | addclpr 11013 |
. . . . . . 7
⊢
(((1P ·P
(1P +P
1P)) ∈ P ∧
((1P +P
1P) ·P
1P) ∈ P) →
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P)) ∈ P) |
30 | 26, 28, 29 | mp2an 691 |
. . . . . 6
⊢
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P)) ∈ P |
31 | | enreceq 11061 |
. . . . . 6
⊢
((((1P +P
1P) ∈ P ∧
1P ∈ P) ∧
(((1P ·P
1P) +P
((1P +P
1P) ·P
(1P +P
1P))) ∈ P ∧
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P)) ∈ P)) →
([⟨(1P +P
1P), 1P⟩]
~R = [⟨((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P))),
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))⟩] ~R ↔
((1P +P
1P) +P
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))) = (1P
+P ((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P)))))) |
32 | 6, 4, 24, 30, 31 | mp4an 692 |
. . . . 5
⊢
([⟨(1P +P
1P), 1P⟩]
~R = [⟨((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P))),
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))⟩] ~R ↔
((1P +P
1P) +P
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))) = (1P
+P ((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P))))) |
33 | 18, 32 | mpbir 230 |
. . . 4
⊢
[⟨(1P +P
1P), 1P⟩]
~R = [⟨((1P
·P 1P)
+P ((1P
+P 1P)
·P (1P
+P 1P))),
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P))⟩]
~R |
34 | 8, 33 | eqtr4i 2764 |
. . 3
⊢
([⟨1P, (1P
+P 1P)⟩]
~R ·R
[⟨1P, (1P
+P 1P)⟩]
~R ) = [⟨(1P
+P 1P),
1P⟩] ~R |
35 | 3, 34 | eqtr4i 2764 |
. 2
⊢
1R = ([⟨1P,
(1P +P
1P)⟩] ~R
·R [⟨1P,
(1P +P
1P)⟩] ~R
) |
36 | 2, 35 | eqtr4i 2764 |
1
⊢
(-1R ·R
-1R) = 1R |