Step | Hyp | Ref
| Expression |
1 | | df-nr 7676 |
. 2
⊢
R = ((P × P) /
~R ) |
2 | | oveq1 5857 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → ([〈𝑥, 𝑦〉] ~R
·R 1R) = (𝐴
·R
1R)) |
3 | | id 19 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → [〈𝑥, 𝑦〉] ~R = 𝐴) |
4 | 2, 3 | eqeq12d 2185 |
. 2
⊢
([〈𝑥, 𝑦〉]
~R = 𝐴 → (([〈𝑥, 𝑦〉] ~R
·R 1R) = [〈𝑥, 𝑦〉] ~R ↔
(𝐴
·R 1R) = 𝐴)) |
5 | | df-1r 7681 |
. . . 4
⊢
1R = [〈(1P
+P 1P),
1P〉] ~R |
6 | 5 | oveq2i 5861 |
. . 3
⊢
([〈𝑥, 𝑦〉]
~R ·R
1R) = ([〈𝑥, 𝑦〉] ~R
·R [〈(1P
+P 1P),
1P〉] ~R
) |
7 | | 1pr 7503 |
. . . . . 6
⊢
1P ∈ P |
8 | | addclpr 7486 |
. . . . . 6
⊢
((1P ∈ P ∧
1P ∈ P) →
(1P +P
1P) ∈ P) |
9 | 7, 7, 8 | mp2an 424 |
. . . . 5
⊢
(1P +P
1P) ∈ P |
10 | | mulsrpr 7695 |
. . . . 5
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ ((1P +P
1P) ∈ P ∧
1P ∈ P)) → ([〈𝑥, 𝑦〉] ~R
·R [〈(1P
+P 1P),
1P〉] ~R ) =
[〈((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)), ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))〉] ~R
) |
11 | 9, 7, 10 | mpanr12 437 |
. . . 4
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ([〈𝑥, 𝑦〉]
~R ·R
[〈(1P +P
1P), 1P〉]
~R ) = [〈((𝑥 ·P
(1P +P
1P)) +P (𝑦 ·P
1P)), ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))〉] ~R
) |
12 | | distrprg 7537 |
. . . . . . . . 9
⊢ ((𝑥 ∈ P ∧
1P ∈ P ∧
1P ∈ P) → (𝑥 ·P
(1P +P
1P)) = ((𝑥 ·P
1P) +P (𝑥 ·P
1P))) |
13 | 7, 7, 12 | mp3an23 1324 |
. . . . . . . 8
⊢ (𝑥 ∈ P →
(𝑥
·P (1P
+P 1P)) = ((𝑥
·P 1P)
+P (𝑥 ·P
1P))) |
14 | | 1idpr 7541 |
. . . . . . . . 9
⊢ (𝑥 ∈ P →
(𝑥
·P 1P) = 𝑥) |
15 | 14 | oveq1d 5865 |
. . . . . . . 8
⊢ (𝑥 ∈ P →
((𝑥
·P 1P)
+P (𝑥 ·P
1P)) = (𝑥 +P (𝑥
·P
1P))) |
16 | 13, 15 | eqtr2d 2204 |
. . . . . . 7
⊢ (𝑥 ∈ P →
(𝑥
+P (𝑥 ·P
1P)) = (𝑥 ·P
(1P +P
1P))) |
17 | | distrprg 7537 |
. . . . . . . . 9
⊢ ((𝑦 ∈ P ∧
1P ∈ P ∧
1P ∈ P) → (𝑦 ·P
(1P +P
1P)) = ((𝑦 ·P
1P) +P (𝑦 ·P
1P))) |
18 | 7, 7, 17 | mp3an23 1324 |
. . . . . . . 8
⊢ (𝑦 ∈ P →
(𝑦
·P (1P
+P 1P)) = ((𝑦
·P 1P)
+P (𝑦 ·P
1P))) |
19 | | 1idpr 7541 |
. . . . . . . . 9
⊢ (𝑦 ∈ P →
(𝑦
·P 1P) = 𝑦) |
20 | 19 | oveq1d 5865 |
. . . . . . . 8
⊢ (𝑦 ∈ P →
((𝑦
·P 1P)
+P (𝑦 ·P
1P)) = (𝑦 +P (𝑦
·P
1P))) |
21 | 18, 20 | eqtrd 2203 |
. . . . . . 7
⊢ (𝑦 ∈ P →
(𝑦
·P (1P
+P 1P)) = (𝑦 +P (𝑦
·P
1P))) |
22 | 16, 21 | oveqan12d 5869 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ((𝑥
+P (𝑥 ·P
1P)) +P (𝑦 ·P
(1P +P
1P))) = ((𝑥 ·P
(1P +P
1P)) +P (𝑦 +P (𝑦
·P
1P)))) |
23 | | simpl 108 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ 𝑥 ∈
P) |
24 | | mulclpr 7521 |
. . . . . . . 8
⊢ ((𝑥 ∈ P ∧
1P ∈ P) → (𝑥 ·P
1P) ∈ P) |
25 | 23, 7, 24 | sylancl 411 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ (𝑥
·P 1P) ∈
P) |
26 | | mulclpr 7521 |
. . . . . . . . 9
⊢ ((𝑦 ∈ P ∧
(1P +P
1P) ∈ P) → (𝑦 ·P
(1P +P
1P)) ∈ P) |
27 | 9, 26 | mpan2 423 |
. . . . . . . 8
⊢ (𝑦 ∈ P →
(𝑦
·P (1P
+P 1P)) ∈
P) |
28 | 27 | adantl 275 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ (𝑦
·P (1P
+P 1P)) ∈
P) |
29 | | addassprg 7528 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
(𝑥
·P 1P) ∈
P ∧ (𝑦
·P (1P
+P 1P)) ∈
P) → ((𝑥
+P (𝑥 ·P
1P)) +P (𝑦 ·P
(1P +P
1P))) = (𝑥 +P ((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P))))) |
30 | 23, 25, 28, 29 | syl3anc 1233 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ((𝑥
+P (𝑥 ·P
1P)) +P (𝑦 ·P
(1P +P
1P))) = (𝑥 +P ((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P))))) |
31 | | mulclpr 7521 |
. . . . . . . 8
⊢ ((𝑥 ∈ P ∧
(1P +P
1P) ∈ P) → (𝑥 ·P
(1P +P
1P)) ∈ P) |
32 | 23, 9, 31 | sylancl 411 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ (𝑥
·P (1P
+P 1P)) ∈
P) |
33 | | simpr 109 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ 𝑦 ∈
P) |
34 | | mulclpr 7521 |
. . . . . . . 8
⊢ ((𝑦 ∈ P ∧
1P ∈ P) → (𝑦 ·P
1P) ∈ P) |
35 | 33, 7, 34 | sylancl 411 |
. . . . . . 7
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ (𝑦
·P 1P) ∈
P) |
36 | | addcomprg 7527 |
. . . . . . . 8
⊢ ((𝑧 ∈ P ∧
𝑤 ∈ P)
→ (𝑧
+P 𝑤) = (𝑤 +P 𝑧)) |
37 | 36 | adantl 275 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P)) → (𝑧 +P 𝑤) = (𝑤 +P 𝑧)) |
38 | | addassprg 7528 |
. . . . . . . 8
⊢ ((𝑧 ∈ P ∧
𝑤 ∈ P
∧ 𝑣 ∈
P) → ((𝑧
+P 𝑤) +P 𝑣) = (𝑧 +P (𝑤 +P
𝑣))) |
39 | 38 | adantl 275 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑧 ∈
P ∧ 𝑤
∈ P ∧ 𝑣 ∈ P)) → ((𝑧 +P
𝑤)
+P 𝑣) = (𝑧 +P (𝑤 +P
𝑣))) |
40 | 32, 33, 35, 37, 39 | caov12d 6031 |
. . . . . 6
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ((𝑥
·P (1P
+P 1P))
+P (𝑦 +P (𝑦
·P 1P))) = (𝑦 +P
((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)))) |
41 | 22, 30, 40 | 3eqtr3d 2211 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ (𝑥
+P ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))) = (𝑦 +P ((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)))) |
42 | 9, 31 | mpan2 423 |
. . . . . . . . 9
⊢ (𝑥 ∈ P →
(𝑥
·P (1P
+P 1P)) ∈
P) |
43 | 7, 34 | mpan2 423 |
. . . . . . . . 9
⊢ (𝑦 ∈ P →
(𝑦
·P 1P) ∈
P) |
44 | | addclpr 7486 |
. . . . . . . . 9
⊢ (((𝑥
·P (1P
+P 1P)) ∈
P ∧ (𝑦
·P 1P) ∈
P) → ((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)) ∈ P) |
45 | 42, 43, 44 | syl2an 287 |
. . . . . . . 8
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)) ∈ P) |
46 | 7, 24 | mpan2 423 |
. . . . . . . . 9
⊢ (𝑥 ∈ P →
(𝑥
·P 1P) ∈
P) |
47 | | addclpr 7486 |
. . . . . . . . 9
⊢ (((𝑥
·P 1P) ∈
P ∧ (𝑦
·P (1P
+P 1P)) ∈
P) → ((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P))) ∈ P) |
48 | 46, 27, 47 | syl2an 287 |
. . . . . . . 8
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P))) ∈ P) |
49 | 45, 48 | anim12i 336 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P)) → (((𝑥 ·P
(1P +P
1P)) +P (𝑦 ·P
1P)) ∈ P ∧ ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P))) ∈ P)) |
50 | | enreceq 7685 |
. . . . . . 7
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)) ∈ P ∧ ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P))) ∈ P)) → ([〈𝑥, 𝑦〉] ~R =
[〈((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)), ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))〉] ~R ↔ (𝑥 +P
((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P)))) = (𝑦 +P ((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P))))) |
51 | 49, 50 | syldan 280 |
. . . . . 6
⊢ (((𝑥 ∈ P ∧
𝑦 ∈ P)
∧ (𝑥 ∈
P ∧ 𝑦
∈ P)) → ([〈𝑥, 𝑦〉] ~R =
[〈((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P)), ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))〉] ~R ↔ (𝑥 +P
((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P)))) = (𝑦 +P ((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P))))) |
52 | 51 | anidms 395 |
. . . . 5
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ([〈𝑥, 𝑦〉]
~R = [〈((𝑥 ·P
(1P +P
1P)) +P (𝑦 ·P
1P)), ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))〉] ~R ↔ (𝑥 +P
((𝑥
·P 1P)
+P (𝑦 ·P
(1P +P
1P)))) = (𝑦 +P ((𝑥
·P (1P
+P 1P))
+P (𝑦 ·P
1P))))) |
53 | 41, 52 | mpbird 166 |
. . . 4
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ [〈𝑥, 𝑦〉]
~R = [〈((𝑥 ·P
(1P +P
1P)) +P (𝑦 ·P
1P)), ((𝑥 ·P
1P) +P (𝑦 ·P
(1P +P
1P)))〉] ~R
) |
54 | 11, 53 | eqtr4d 2206 |
. . 3
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ([〈𝑥, 𝑦〉]
~R ·R
[〈(1P +P
1P), 1P〉]
~R ) = [〈𝑥, 𝑦〉] ~R
) |
55 | 6, 54 | eqtrid 2215 |
. 2
⊢ ((𝑥 ∈ P ∧
𝑦 ∈ P)
→ ([〈𝑥, 𝑦〉]
~R ·R
1R) = [〈𝑥, 𝑦〉] ~R
) |
56 | 1, 4, 55 | ecoptocl 6596 |
1
⊢ (𝐴 ∈ R →
(𝐴
·R 1R) = 𝐴) |