Proof of Theorem m1m1sr
| Step | Hyp | Ref
| Expression |
| 1 | | df-m1r 11102 |
. . 3
⊢
-1R = [〈1P,
(1P +P
1P)〉]
~R |
| 2 | 1, 1 | oveq12i 7443 |
. 2
⊢
(-1R ·R
-1R) = ([〈1P,
(1P +P
1P)〉] ~R
·R [〈1P,
(1P +P
1P)〉] ~R
) |
| 3 | | df-1r 11101 |
. . 3
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R |
| 4 | | 1pr 11055 |
. . . . 5
⊢
1P ∈ P |
| 5 | | addclpr 11058 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
| 6 | 4, 4, 5 | mp2an 692 |
. . . . 5
⊢
(1P +P
1P) ∈ P |
| 7 | | mulsrpr 11116 |
. . . . 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 11062 |
. . . . . 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 11069 |
. . . . . . . . 9
⊢
(1P ∈ P →
(1P ·P
1P) = 1P) |
| 11 | 4, 10 | ax-mp 5 |
. . . . . . . 8
⊢
(1P ·P
1P) = 1P |
| 12 | | distrpr 11068 |
. . . . . . . . 9
⊢
((1P +P
1P) ·P
(1P +P
1P)) = (((1P
+P 1P)
·P 1P)
+P ((1P
+P 1P)
·P
1P)) |
| 13 | | mulcompr 11063 |
. . . . . . . . . 10
⊢
(1P ·P
(1P +P
1P)) = ((1P
+P 1P)
·P
1P) |
| 14 | 13 | oveq1i 7441 |
. . . . . . . . 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 7443 |
. . . . . . 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 7442 |
. . . . . 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 11060 |
. . . . . . . 8
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P ·P
1P) ∈ P) |
| 20 | 4, 4, 19 | mp2an 692 |
. . . . . . 7
⊢
(1P ·P
1P) ∈ P |
| 21 | | mulclpr 11060 |
. . . . . . . 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 11058 |
. . . . . . 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 11060 |
. . . . . . . 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 11060 |
. . . . . . . 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 11058 |
. . . . . . 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 11106 |
. . . . . 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 231 |
. . . 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 |