Proof of Theorem m1m1sr
Step | Hyp | Ref
| Expression |
1 | | df-m1r 10676 |
. . 3
⊢
-1R = [〈1P,
(1P +P
1P)〉]
~R |
2 | 1, 1 | oveq12i 7225 |
. 2
⊢
(-1R ·R
-1R) = ([〈1P,
(1P +P
1P)〉] ~R
·R [〈1P,
(1P +P
1P)〉] ~R
) |
3 | | df-1r 10675 |
. . 3
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R |
4 | | 1pr 10629 |
. . . . 5
⊢
1P ∈ P |
5 | | addclpr 10632 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
6 | 4, 4, 5 | mp2an 692 |
. . . . 5
⊢
(1P +P
1P) ∈ P |
7 | | mulsrpr 10690 |
. . . . 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 693 |
. . . 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 10636 |
. . . . . 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 10643 |
. . . . . . . . 9
⊢
(1P ∈ P →
(1P ·P
1P) = 1P) |
11 | 4, 10 | ax-mp 5 |
. . . . . . . 8
⊢
(1P ·P
1P) = 1P |
12 | | distrpr 10642 |
. . . . . . . . 9
⊢
((1P +P
1P) ·P
(1P +P
1P)) = (((1P
+P 1P)
·P 1P)
+P ((1P
+P 1P)
·P
1P)) |
13 | | mulcompr 10637 |
. . . . . . . . . 10
⊢
(1P ·P
(1P +P
1P)) = ((1P
+P 1P)
·P
1P) |
14 | 13 | oveq1i 7223 |
. . . . . . . . 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 2768 |
. . . . . . . 8
⊢
((1P +P
1P) ·P
(1P +P
1P)) = ((1P
·P (1P
+P 1P))
+P ((1P
+P 1P)
·P
1P)) |
16 | 11, 15 | oveq12i 7225 |
. . . . . . 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 7224 |
. . . . . 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 2768 |
. . . . 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 10634 |
. . . . . . . 8
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P ·P
1P) ∈ P) |
20 | 4, 4, 19 | mp2an 692 |
. . . . . . 7
⊢
(1P ·P
1P) ∈ P |
21 | | mulclpr 10634 |
. . . . . . . 8
⊢
(((1P +P
1P) ∈ P ∧
(1P +P
1P) ∈ P) →
((1P +P
1P) ·P
(1P +P
1P)) ∈ P) |
22 | 6, 6, 21 | mp2an 692 |
. . . . . . 7
⊢
((1P +P
1P) ·P
(1P +P
1P)) ∈ P |
23 | | addclpr 10632 |
. . . . . . 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 692 |
. . . . . 6
⊢
((1P ·P
1P) +P
((1P +P
1P) ·P
(1P +P
1P))) ∈ P |
25 | | mulclpr 10634 |
. . . . . . . 8
⊢
((1P ∈ P ∧
(1P +P
1P) ∈ P) →
(1P ·P
(1P +P
1P)) ∈ P) |
26 | 4, 6, 25 | mp2an 692 |
. . . . . . 7
⊢
(1P ·P
(1P +P
1P)) ∈ P |
27 | | mulclpr 10634 |
. . . . . . . 8
⊢
(((1P +P
1P) ∈ P ∧
1P ∈ P) →
((1P +P
1P) ·P
1P) ∈ P) |
28 | 6, 4, 27 | mp2an 692 |
. . . . . . 7
⊢
((1P +P
1P) ·P
1P) ∈ P |
29 | | addclpr 10632 |
. . . . . . 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 692 |
. . . . . 6
⊢
((1P ·P
(1P +P
1P)) +P
((1P +P
1P) ·P
1P)) ∈ P |
31 | | enreceq 10680 |
. . . . . 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 693 |
. . . . 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 234 |
. . . 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 2768 |
. . 3
⊢
([〈1P, (1P
+P 1P)〉]
~R ·R
[〈1P, (1P
+P 1P)〉]
~R ) = [〈(1P
+P 1P),
1P〉] ~R |
35 | 3, 34 | eqtr4i 2768 |
. 2
⊢
1R = ([〈1P,
(1P +P
1P)〉] ~R
·R [〈1P,
(1P +P
1P)〉] ~R
) |
36 | 2, 35 | eqtr4i 2768 |
1
⊢
(-1R ·R
-1R) = 1R |