Step | Hyp | Ref
| Expression |
1 | | opelxpi 4319 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P) → 〈A, B〉 ∈ (P ×
P)) |
2 | | enrex 6665 |
. . . . 5
⊢
~R ∈
V |
3 | 2 | ecelqsi 6096 |
. . . 4
⊢
(〈A, B〉 ∈
(P × P) → [〈A, B〉]
~R ∈
((P × P) / ~R
)) |
4 | 1, 3 | syl 14 |
. . 3
⊢
((A ∈ P ∧ B ∈ P) → [〈A, B〉]
~R ∈
((P × P) / ~R
)) |
5 | | opelxpi 4319 |
. . . 4
⊢ ((𝐶 ∈ P ∧ 𝐷 ∈
P) → 〈𝐶, 𝐷〉 ∈
(P × P)) |
6 | 2 | ecelqsi 6096 |
. . . 4
⊢
(〈𝐶, 𝐷〉 ∈ (P × P) →
[〈𝐶, 𝐷〉] ~R ∈ ((P × P)
/ ~R )) |
7 | 5, 6 | syl 14 |
. . 3
⊢ ((𝐶 ∈ P ∧ 𝐷 ∈
P) → [〈𝐶, 𝐷〉] ~R ∈ ((P × P)
/ ~R )) |
8 | 4, 7 | anim12i 321 |
. 2
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → ([〈A,
B〉] ~R ∈ ((P × P)
/ ~R ) ∧
[〈𝐶, 𝐷〉] ~R ∈ ((P × P)
/ ~R ))) |
9 | | eqid 2037 |
. . . 4
⊢
[〈A, B〉] ~R =
[〈A, B〉]
~R |
10 | | eqid 2037 |
. . . 4
⊢
[〈𝐶, 𝐷〉]
~R = [〈𝐶, 𝐷〉]
~R |
11 | 9, 10 | pm3.2i 257 |
. . 3
⊢
([〈A, B〉] ~R =
[〈A, B〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
) |
12 | | eqid 2037 |
. . 3
⊢
[〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(A +P 𝐶), (B +P 𝐷)〉]
~R |
13 | | opeq12 3542 |
. . . . . . . . 9
⊢
((w = A ∧ v = B) →
〈w, v〉 = 〈A, B〉) |
14 | 13 | eceq1d 6078 |
. . . . . . . 8
⊢
((w = A ∧ v = B) →
[〈w, v〉] ~R =
[〈A, B〉] ~R
) |
15 | 14 | eqeq2d 2048 |
. . . . . . 7
⊢
((w = A ∧ v = B) →
([〈A, B〉] ~R =
[〈w, v〉] ~R ↔
[〈A, B〉] ~R =
[〈A, B〉] ~R
)) |
16 | 15 | anbi1d 438 |
. . . . . 6
⊢
((w = A ∧ v = B) →
(([〈A, B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ↔
([〈A, B〉] ~R =
[〈A, B〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
))) |
17 | | simpl 102 |
. . . . . . . . . 10
⊢
((w = A ∧ v = B) →
w = A) |
18 | 17 | oveq1d 5470 |
. . . . . . . . 9
⊢
((w = A ∧ v = B) →
(w +P 𝐶) = (A +P 𝐶)) |
19 | | simpr 103 |
. . . . . . . . . 10
⊢
((w = A ∧ v = B) →
v = B) |
20 | 19 | oveq1d 5470 |
. . . . . . . . 9
⊢
((w = A ∧ v = B) →
(v +P 𝐷) = (B +P 𝐷)) |
21 | 18, 20 | opeq12d 3548 |
. . . . . . . 8
⊢
((w = A ∧ v = B) →
〈(w +P 𝐶), (v +P 𝐷)〉 = 〈(A +P 𝐶), (B
+P 𝐷)〉) |
22 | 21 | eceq1d 6078 |
. . . . . . 7
⊢
((w = A ∧ v = B) →
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R
) |
23 | 22 | eqeq2d 2048 |
. . . . . 6
⊢
((w = A ∧ v = B) →
([〈(A +P
𝐶), (B +P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R ↔
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R
)) |
24 | 16, 23 | anbi12d 442 |
. . . . 5
⊢
((w = A ∧ v = B) →
((([〈A, B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R )
↔ (([〈A, B〉] ~R =
[〈A, B〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R
))) |
25 | 24 | spc2egv 2636 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P) → ((([〈A, B〉]
~R = [〈A,
B〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ ∃w∃v(([〈A,
B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R
))) |
26 | | opeq12 3542 |
. . . . . . . . . 10
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → 〈u, 𝑡〉 = 〈𝐶, 𝐷〉) |
27 | 26 | eceq1d 6078 |
. . . . . . . . 9
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → [〈u, 𝑡〉] ~R =
[〈𝐶, 𝐷〉] ~R
) |
28 | 27 | eqeq2d 2048 |
. . . . . . . 8
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → ([〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ↔
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
)) |
29 | 28 | anbi2d 437 |
. . . . . . 7
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → (([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ↔
([〈A, B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
))) |
30 | | simpl 102 |
. . . . . . . . . . 11
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → u = 𝐶) |
31 | 30 | oveq2d 5471 |
. . . . . . . . . 10
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → (w +P u) = (w
+P 𝐶)) |
32 | | simpr 103 |
. . . . . . . . . . 11
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → 𝑡 = 𝐷) |
33 | 32 | oveq2d 5471 |
. . . . . . . . . 10
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → (v +P 𝑡) = (v
+P 𝐷)) |
34 | 31, 33 | opeq12d 3548 |
. . . . . . . . 9
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → 〈(w +P u), (v
+P 𝑡)〉 = 〈(w +P 𝐶), (v
+P 𝐷)〉) |
35 | 34 | eceq1d 6078 |
. . . . . . . 8
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → [〈(w +P u), (v
+P 𝑡)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R
) |
36 | 35 | eqeq2d 2048 |
. . . . . . 7
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → ([〈(A +P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ↔
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R
)) |
37 | 29, 36 | anbi12d 442 |
. . . . . 6
⊢
((u = 𝐶 ∧ 𝑡 = 𝐷) → ((([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ) ↔
(([〈A, B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R
))) |
38 | 37 | spc2egv 2636 |
. . . . 5
⊢ ((𝐶 ∈ P ∧ 𝐷 ∈
P) → ((([〈A,
B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R )
→ ∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))) |
39 | 38 | 2eximdv 1759 |
. . . 4
⊢ ((𝐶 ∈ P ∧ 𝐷 ∈
P) → (∃w∃v(([〈A,
B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P 𝐶), (v +P 𝐷)〉] ~R )
→ ∃w∃v∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))) |
40 | 25, 39 | sylan9 389 |
. . 3
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → ((([〈A,
B〉] ~R =
[〈A, B〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ ∃w∃v∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))) |
41 | 11, 12, 40 | mp2ani 408 |
. 2
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → ∃w∃v∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
)) |
42 | | ecexg 6046 |
. . . 4
⊢ (
~R ∈ V →
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R ∈ V) |
43 | 2, 42 | ax-mp 7 |
. . 3
⊢
[〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R ∈ V |
44 | | simp1 903 |
. . . . . . . 8
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ x = [〈A, B〉]
~R ) |
45 | 44 | eqeq1d 2045 |
. . . . . . 7
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ (x = [〈w, v〉]
~R ↔ [〈A, B〉]
~R = [〈w,
v〉] ~R
)) |
46 | | simp2 904 |
. . . . . . . 8
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ y = [〈𝐶, 𝐷〉] ~R
) |
47 | 46 | eqeq1d 2045 |
. . . . . . 7
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ (y = [〈u, 𝑡〉] ~R ↔
[〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R
)) |
48 | 45, 47 | anbi12d 442 |
. . . . . 6
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ ((x = [〈w, v〉]
~R ∧ y = [〈u,
𝑡〉]
~R ) ↔ ([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R
))) |
49 | | simp3 905 |
. . . . . . 7
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ z = [〈(A +P 𝐶), (B
+P 𝐷)〉] ~R
) |
50 | 49 | eqeq1d 2045 |
. . . . . 6
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ (z = [〈(w +P u), (v
+P 𝑡)〉] ~R ↔
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
)) |
51 | 48, 50 | anbi12d 442 |
. . . . 5
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ (((x = [〈w, v〉]
~R ∧ y = [〈u,
𝑡〉]
~R ) ∧ z = [〈(w
+P u), (v +P 𝑡)〉] ~R ) ↔
(([〈A, B〉] ~R =
[〈w, v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))) |
52 | 51 | 4exbidv 1747 |
. . . 4
⊢
((x = [〈A, B〉]
~R ∧ y = [〈𝐶, 𝐷〉] ~R ∧ z =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R )
→ (∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ) ↔
∃w∃v∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))) |
53 | | addsrmo 6671 |
. . . 4
⊢
((x ∈ ((P × P)
/ ~R ) ∧
y ∈
((P × P) / ~R
)) → ∃*z∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
)) |
54 | | df-plr 6656 |
. . . . 5
⊢
+R = {〈〈x, y〉,
z〉 ∣ ((x ∈
R ∧ y ∈
R) ∧ ∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))} |
55 | | df-nr 6655 |
. . . . . . . . 9
⊢
R = ((P × P) /
~R ) |
56 | 55 | eleq2i 2101 |
. . . . . . . 8
⊢ (x ∈
R ↔ x ∈ ((P × P)
/ ~R )) |
57 | 55 | eleq2i 2101 |
. . . . . . . 8
⊢ (y ∈
R ↔ y ∈ ((P × P)
/ ~R )) |
58 | 56, 57 | anbi12i 433 |
. . . . . . 7
⊢
((x ∈ R ∧ y ∈ R) ↔ (x ∈
((P × P) / ~R
) ∧ y
∈ ((P × P)
/ ~R ))) |
59 | 58 | anbi1i 431 |
. . . . . 6
⊢
(((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ))
↔ ((x ∈ ((P × P)
/ ~R ) ∧
y ∈
((P × P) / ~R
)) ∧ ∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))) |
60 | 59 | oprabbii 5502 |
. . . . 5
⊢
{〈〈x, y〉, z〉
∣ ((x ∈ R ∧ y ∈ R) ∧ ∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ))} =
{〈〈x, y〉, z〉
∣ ((x ∈ ((P × P)
/ ~R ) ∧
y ∈
((P × P) / ~R
)) ∧ ∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))} |
61 | 54, 60 | eqtri 2057 |
. . . 4
⊢
+R = {〈〈x, y〉,
z〉 ∣ ((x ∈
((P × P) / ~R
) ∧ y
∈ ((P × P)
/ ~R )) ∧
∃w∃v∃u∃𝑡((x =
[〈w, v〉] ~R ∧ y =
[〈u, 𝑡〉] ~R ) ∧ z =
[〈(w +P
u), (v
+P 𝑡)〉] ~R
))} |
62 | 52, 53, 61 | ovig 5564 |
. . 3
⊢
(([〈A, B〉] ~R ∈ ((P × P)
/ ~R ) ∧
[〈𝐶, 𝐷〉] ~R ∈ ((P × P)
/ ~R ) ∧
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R ∈ V) → (∃w∃v∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ) →
([〈A, B〉] ~R
+R [〈𝐶, 𝐷〉] ~R ) =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R
)) |
63 | 43, 62 | mp3an3 1220 |
. 2
⊢
(([〈A, B〉] ~R ∈ ((P × P)
/ ~R ) ∧
[〈𝐶, 𝐷〉] ~R ∈ ((P × P)
/ ~R )) → (∃w∃v∃u∃𝑡(([〈A, B〉]
~R = [〈w,
v〉] ~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈u, 𝑡〉] ~R ) ∧ [〈(A
+P 𝐶), (B
+P 𝐷)〉] ~R =
[〈(w +P
u), (v
+P 𝑡)〉] ~R ) →
([〈A, B〉] ~R
+R [〈𝐶, 𝐷〉] ~R ) =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R
)) |
64 | 8, 41, 63 | sylc 56 |
1
⊢
(((A ∈ P ∧ B ∈ P) ∧ (𝐶 ∈
P ∧ 𝐷 ∈
P)) → ([〈A,
B〉] ~R
+R [〈𝐶, 𝐷〉] ~R ) =
[〈(A +P 𝐶), (B +P 𝐷)〉] ~R
) |