Step | Hyp | Ref
| Expression |
1 | | df-nr 6655 |
. 2
⊢
R = ((P × P) /
~R ) |
2 | | oveq1 5462 |
. . 3
⊢
([〈x, y〉] ~R = A → ([〈x, y〉]
~R ·R
0R) = (A
·R
0R)) |
3 | 2 | eqeq1d 2045 |
. 2
⊢
([〈x, y〉] ~R = A → (([〈x, y〉]
~R ·R
0R) = 0R ↔ (A ·R
0R) = 0R)) |
4 | | 1pr 6535 |
. . . . 5
⊢
1P ∈
P |
5 | | mulsrpr 6674 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (1P ∈ P ∧ 1P ∈ P)) → ([〈x, y〉]
~R ·R
[〈1P, 1P〉]
~R ) = [〈((x
·P 1P)
+P (y
·P 1P)), ((x ·P
1P) +P (y ·P
1P))〉] ~R
) |
6 | 4, 4, 5 | mpanr12 415 |
. . . 4
⊢
((x ∈ P ∧ y ∈ P) → ([〈x, y〉]
~R ·R
[〈1P, 1P〉]
~R ) = [〈((x
·P 1P)
+P (y
·P 1P)), ((x ·P
1P) +P (y ·P
1P))〉] ~R
) |
7 | | mulclpr 6553 |
. . . . . . . . . 10
⊢
((x ∈ P ∧ 1P ∈ P) → (x ·P
1P) ∈
P) |
8 | 4, 7 | mpan2 401 |
. . . . . . . . 9
⊢ (x ∈
P → (x
·P 1P) ∈ P) |
9 | | mulclpr 6553 |
. . . . . . . . . 10
⊢
((y ∈ P ∧ 1P ∈ P) → (y ·P
1P) ∈
P) |
10 | 4, 9 | mpan2 401 |
. . . . . . . . 9
⊢ (y ∈
P → (y
·P 1P) ∈ P) |
11 | | addclpr 6520 |
. . . . . . . . 9
⊢
(((x
·P 1P) ∈ P ∧ (y
·P 1P) ∈ P) → ((x ·P
1P) +P (y ·P
1P)) ∈
P) |
12 | 8, 10, 11 | syl2an 273 |
. . . . . . . 8
⊢
((x ∈ P ∧ y ∈ P) → ((x ·P
1P) +P (y ·P
1P)) ∈
P) |
13 | 12, 12 | anim12i 321 |
. . . . . . 7
⊢
(((x ∈ P ∧ y ∈ P) ∧ (x ∈ P ∧ y ∈ P)) → (((x ·P
1P) +P (y ·P
1P)) ∈
P ∧ ((x ·P
1P) +P (y ·P
1P)) ∈
P)) |
14 | | eqid 2037 |
. . . . . . . 8
⊢
(((x
·P 1P)
+P (y
·P 1P))
+P 1P) = (((x ·P
1P) +P (y ·P
1P)) +P
1P) |
15 | | enreceq 6664 |
. . . . . . . 8
⊢
(((((x
·P 1P)
+P (y
·P 1P)) ∈ P ∧ ((x
·P 1P)
+P (y
·P 1P)) ∈ P) ∧ (1P ∈ P ∧ 1P ∈ P)) → ([〈((x ·P
1P) +P (y ·P
1P)), ((x
·P 1P)
+P (y
·P 1P))〉]
~R = [〈1P,
1P〉] ~R ↔
(((x ·P
1P) +P (y ·P
1P)) +P
1P) = (((x
·P 1P)
+P (y
·P 1P))
+P 1P))) |
16 | 14, 15 | mpbiri 157 |
. . . . . . 7
⊢
(((((x
·P 1P)
+P (y
·P 1P)) ∈ P ∧ ((x
·P 1P)
+P (y
·P 1P)) ∈ P) ∧ (1P ∈ P ∧ 1P ∈ P)) → [〈((x ·P
1P) +P (y ·P
1P)), ((x
·P 1P)
+P (y
·P 1P))〉]
~R = [〈1P,
1P〉] ~R
) |
17 | 13, 16 | sylan 267 |
. . . . . 6
⊢
((((x ∈ P ∧ y ∈ P) ∧ (x ∈ P ∧ y ∈ P)) ∧ (1P ∈ P ∧ 1P ∈ P)) → [〈((x ·P
1P) +P (y ·P
1P)), ((x
·P 1P)
+P (y
·P 1P))〉]
~R = [〈1P,
1P〉] ~R
) |
18 | 4, 4, 17 | mpanr12 415 |
. . . . 5
⊢
(((x ∈ P ∧ y ∈ P) ∧ (x ∈ P ∧ y ∈ P)) → [〈((x ·P
1P) +P (y ·P
1P)), ((x
·P 1P)
+P (y
·P 1P))〉]
~R = [〈1P,
1P〉] ~R
) |
19 | 18 | anidms 377 |
. . . 4
⊢
((x ∈ P ∧ y ∈ P) → [〈((x ·P
1P) +P (y ·P
1P)), ((x
·P 1P)
+P (y
·P 1P))〉]
~R = [〈1P,
1P〉] ~R
) |
20 | 6, 19 | eqtrd 2069 |
. . 3
⊢
((x ∈ P ∧ y ∈ P) → ([〈x, y〉]
~R ·R
[〈1P, 1P〉]
~R ) = [〈1P,
1P〉] ~R
) |
21 | | df-0r 6659 |
. . . 4
⊢
0R = [〈1P,
1P〉] ~R |
22 | 21 | oveq2i 5466 |
. . 3
⊢
([〈x, y〉] ~R
·R 0R) =
([〈x, y〉] ~R
·R [〈1P,
1P〉] ~R
) |
23 | 20, 22, 21 | 3eqtr4g 2094 |
. 2
⊢
((x ∈ P ∧ y ∈ P) → ([〈x, y〉]
~R ·R
0R) = 0R) |
24 | 1, 3, 23 | ecoptocl 6129 |
1
⊢ (A ∈
R → (A
·R 0R) =
0R) |