Step | Hyp | Ref
| Expression |
1 | | enrer 7697 |
. . . . . . . . . . . . . . . 16
⊢
~R Er (P ×
P) |
2 | 1 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
~R Er (P ×
P)) |
3 | | prsrlem1 7704 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
((((𝑤 ∈
P ∧ 𝑣
∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧
((𝑢 ∈ P
∧ 𝑡 ∈
P) ∧ (𝑔
∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P
𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔)))) |
4 | | addcmpblnr 7701 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑤 ∈ P ∧
𝑣 ∈ P)
∧ (𝑠 ∈
P ∧ 𝑓
∈ P)) ∧ ((𝑢 ∈ P ∧ 𝑡 ∈ P) ∧
(𝑔 ∈ P
∧ ℎ ∈
P))) → (((𝑤 +P 𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔)) → 〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉
~R 〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉)) |
5 | 4 | imp 123 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑤 ∈
P ∧ 𝑣
∈ P) ∧ (𝑠 ∈ P ∧ 𝑓 ∈ P)) ∧
((𝑢 ∈ P
∧ 𝑡 ∈
P) ∧ (𝑔
∈ P ∧ ℎ ∈ P))) ∧ ((𝑤 +P
𝑓) = (𝑣 +P 𝑠) ∧ (𝑢 +P ℎ) = (𝑡 +P 𝑔))) → 〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉
~R 〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉) |
6 | 3, 5 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
〈(𝑤
+P 𝑢), (𝑣 +P 𝑡)〉
~R 〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉) |
7 | 2, 6 | erthi 6559 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈(𝑤
+P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) |
8 | 7 | adantrlr 482 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ (𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
[〈(𝑤
+P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) |
9 | 8 | adantrrr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) |
10 | | simprlr 533 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → 𝑧 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R ) |
11 | | simprrr 535 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → 𝑞 = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) |
12 | 9, 10, 11 | 3eqtr4d 2213 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) → 𝑧 = 𝑞) |
13 | 12 | expr 373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → (((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞)) |
14 | 13 | exlimdvv 1890 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → (∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞)) |
15 | 14 | exlimdvv 1890 |
. . . . . . . 8
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞)) |
16 | 15 | ex 114 |
. . . . . . 7
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
(((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞))) |
17 | 16 | exlimdvv 1890 |
. . . . . 6
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
(∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞))) |
18 | 17 | exlimdvv 1890 |
. . . . 5
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
(∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) → (∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ) → 𝑧 = 𝑞))) |
19 | 18 | impd 252 |
. . . 4
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) |
20 | 19 | alrimivv 1868 |
. . 3
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) |
21 | | opeq12 3767 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈𝑤, 𝑣〉 = 〈𝑠, 𝑓〉) |
22 | 21 | eceq1d 6549 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈𝑤, 𝑣〉] ~R =
[〈𝑠, 𝑓〉]
~R ) |
23 | 22 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝐴 = [〈𝑤, 𝑣〉] ~R ↔
𝐴 = [〈𝑠, 𝑓〉] ~R
)) |
24 | 23 | anbi1d 462 |
. . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R
))) |
25 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑤 = 𝑠) |
26 | 25 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑤 +P 𝑢) = (𝑠 +P 𝑢)) |
27 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑣 = 𝑓) |
28 | 27 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑣 +P 𝑡) = (𝑓 +P 𝑡)) |
29 | 26, 28 | opeq12d 3773 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉 = 〈(𝑠 +P
𝑢), (𝑓 +P 𝑡)〉) |
30 | 29 | eceq1d 6549 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R ) |
31 | 30 | eqeq2d 2182 |
. . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑞 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R ↔ 𝑞 = [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R )) |
32 | 24, 31 | anbi12d 470 |
. . . . . . 7
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑢), (𝑓 +P 𝑡)〉]
~R ))) |
33 | | opeq12 3767 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈𝑢, 𝑡〉 = 〈𝑔, ℎ〉) |
34 | 33 | eceq1d 6549 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈𝑢, 𝑡〉] ~R =
[〈𝑔, ℎ〉]
~R ) |
35 | 34 | eqeq2d 2182 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝐵 = [〈𝑢, 𝑡〉] ~R ↔
𝐵 = [〈𝑔, ℎ〉] ~R
)) |
36 | 35 | anbi2d 461 |
. . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R
))) |
37 | | simpl 108 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑢 = 𝑔) |
38 | 37 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑠 +P 𝑢) = (𝑠 +P 𝑔)) |
39 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑡 = ℎ) |
40 | 39 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑓 +P 𝑡) = (𝑓 +P ℎ)) |
41 | 38, 40 | opeq12d 3773 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉 = 〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉) |
42 | 41 | eceq1d 6549 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R ) |
43 | 42 | eqeq2d 2182 |
. . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑞 = [〈(𝑠 +P 𝑢), (𝑓 +P 𝑡)〉]
~R ↔ 𝑞 = [〈(𝑠 +P 𝑔), (𝑓 +P ℎ)〉]
~R )) |
44 | 36, 43 | anbi12d 470 |
. . . . . . 7
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑢), (𝑓 +P 𝑡)〉]
~R ) ↔ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) |
45 | 32, 44 | cbvex4v 1923 |
. . . . . 6
⊢
(∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) |
46 | 45 | anbi2i 454 |
. . . . 5
⊢
((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) ↔ (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R ))) |
47 | 46 | imbi1i 237 |
. . . 4
⊢
(((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞) ↔ ((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) |
48 | 47 | 2albii 1464 |
. . 3
⊢
(∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞) ↔ ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈(𝑠 +P
𝑔), (𝑓 +P ℎ)〉]
~R )) → 𝑧 = 𝑞)) |
49 | 20, 48 | sylibr 133 |
. 2
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞)) |
50 | | eqeq1 2177 |
. . . . 5
⊢ (𝑧 = 𝑞 → (𝑧 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R ↔ 𝑞 = [〈(𝑤 +P 𝑢), (𝑣 +P 𝑡)〉]
~R )) |
51 | 50 | anbi2d 461 |
. . . 4
⊢ (𝑧 = 𝑞 → (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ))) |
52 | 51 | 4exbidv 1863 |
. . 3
⊢ (𝑧 = 𝑞 → (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ))) |
53 | 52 | mo4 2080 |
. 2
⊢
(∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ↔ ∀𝑧∀𝑞((∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R ) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) → 𝑧 = 𝑞)) |
54 | 49, 53 | sylibr 133 |
1
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈(𝑤 +P
𝑢), (𝑣 +P 𝑡)〉]
~R )) |