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