Step | Hyp | Ref
| Expression |
1 | | enrer 10564 |
. . . . . . . . . . . . . . . 16
⊢
~R Er (P ×
P) |
2 | 1 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) ∧ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ))) →
~R Er (P ×
P)) |
3 | | prsrlem1 10573 |
. . . . . . . . . . . . . . . 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 10572 |
. . . . . . . . . . . . . . . . 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 410 |
. . . . . . . . . . . . . . . 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 17 |
. . . . . . . . . . . . . . 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 8372 |
. . . . . . . . . . . . . 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 723 |
. . . . . . . . . . . . 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 725 |
. . . . . . . . . . . 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 780 |
. . . . . . . . . . . 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 782 |
. . . . . . . . . . . 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 2783 |
. . . . . . . . . . 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 460 |
. . . . . . . . . 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 1940 |
. . . . . . . . 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 1940 |
. . . . . . . 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 416 |
. . . . . . 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 1940 |
. . . . . 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 1940 |
. . . . 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 414 |
. . . 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 1934 |
. . 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 4764 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈𝑤, 𝑣〉 = 〈𝑠, 𝑓〉) |
22 | 21 | eceq1d 8360 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈𝑤, 𝑣〉] ~R =
[〈𝑠, 𝑓〉]
~R ) |
23 | 22 | eqeq2d 2749 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝐴 = [〈𝑤, 𝑣〉] ~R ↔
𝐴 = [〈𝑠, 𝑓〉] ~R
)) |
24 | 23 | anbi1d 633 |
. . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R
))) |
25 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑤 = 𝑠) |
26 | 25 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑤 ·P 𝑢) = (𝑠 ·P 𝑢)) |
27 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 𝑣 = 𝑓) |
28 | 27 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑣 ·P 𝑡) = (𝑓 ·P 𝑡)) |
29 | 26, 28 | oveq12d 7189 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → ((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)) = ((𝑠 ·P 𝑢) +P
(𝑓
·P 𝑡))) |
30 | 25 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑤 ·P 𝑡) = (𝑠 ·P 𝑡)) |
31 | 27 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑣 ·P 𝑢) = (𝑓 ·P 𝑢)) |
32 | 30, 31 | oveq12d 7189 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢)) = ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))) |
33 | 29, 32 | opeq12d 4770 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → 〈((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉 = 〈((𝑠 ·P 𝑢) +P
(𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉) |
34 | 33 | eceq1d 8360 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → [〈((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R =
[〈((𝑠
·P 𝑢) +P (𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉] ~R
) |
35 | 34 | eqeq2d 2749 |
. . . . . . . 8
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (𝑞 = [〈((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R ↔
𝑞 = [〈((𝑠
·P 𝑢) +P (𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉] ~R
)) |
36 | 24, 35 | anbi12d 634 |
. . . . . . 7
⊢ ((𝑤 = 𝑠 ∧ 𝑣 = 𝑓) → (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈((𝑠
·P 𝑢) +P (𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉] ~R
))) |
37 | | opeq12 4764 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈𝑢, 𝑡〉 = 〈𝑔, ℎ〉) |
38 | 37 | eceq1d 8360 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈𝑢, 𝑡〉] ~R =
[〈𝑔, ℎ〉]
~R ) |
39 | 38 | eqeq2d 2749 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝐵 = [〈𝑢, 𝑡〉] ~R ↔
𝐵 = [〈𝑔, ℎ〉] ~R
)) |
40 | 39 | anbi2d 632 |
. . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ↔
(𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R
))) |
41 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑢 = 𝑔) |
42 | 41 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑠 ·P 𝑢) = (𝑠 ·P 𝑔)) |
43 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 𝑡 = ℎ) |
44 | 43 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑓 ·P 𝑡) = (𝑓 ·P ℎ)) |
45 | 42, 44 | oveq12d 7189 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → ((𝑠 ·P 𝑢) +P
(𝑓
·P 𝑡)) = ((𝑠 ·P 𝑔) +P
(𝑓
·P ℎ))) |
46 | 43 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑠 ·P 𝑡) = (𝑠 ·P ℎ)) |
47 | 41 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑓 ·P 𝑢) = (𝑓 ·P 𝑔)) |
48 | 46, 47 | oveq12d 7189 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢)) = ((𝑠 ·P ℎ) +P
(𝑓
·P 𝑔))) |
49 | 45, 48 | opeq12d 4770 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → 〈((𝑠 ·P 𝑢) +P
(𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉 = 〈((𝑠 ·P 𝑔) +P
(𝑓
·P ℎ)), ((𝑠 ·P ℎ) +P
(𝑓
·P 𝑔))〉) |
50 | 49 | eceq1d 8360 |
. . . . . . . . 9
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → [〈((𝑠 ·P 𝑢) +P
(𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉] ~R =
[〈((𝑠
·P 𝑔) +P (𝑓
·P ℎ)), ((𝑠 ·P ℎ) +P
(𝑓
·P 𝑔))〉] ~R
) |
51 | 50 | eqeq2d 2749 |
. . . . . . . 8
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (𝑞 = [〈((𝑠 ·P 𝑢) +P
(𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉] ~R ↔
𝑞 = [〈((𝑠
·P 𝑔) +P (𝑓
·P ℎ)), ((𝑠 ·P ℎ) +P
(𝑓
·P 𝑔))〉] ~R
)) |
52 | 40, 51 | anbi12d 634 |
. . . . . . 7
⊢ ((𝑢 = 𝑔 ∧ 𝑡 = ℎ) → (((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈((𝑠
·P 𝑢) +P (𝑓
·P 𝑡)), ((𝑠 ·P 𝑡) +P
(𝑓
·P 𝑢))〉] ~R )
↔ ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈((𝑠
·P 𝑔) +P (𝑓
·P ℎ)), ((𝑠 ·P ℎ) +P
(𝑓
·P 𝑔))〉] ~R
))) |
53 | 36, 52 | cbvex4vw 2053 |
. . . . . 6
⊢
(∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ ∃𝑠∃𝑓∃𝑔∃ℎ((𝐴 = [〈𝑠, 𝑓〉] ~R ∧
𝐵 = [〈𝑔, ℎ〉] ~R ) ∧
𝑞 = [〈((𝑠
·P 𝑔) +P (𝑓
·P ℎ)), ((𝑠 ·P ℎ) +P
(𝑓
·P 𝑔))〉] ~R
)) |
54 | 53 | anbi2i 626 |
. . . . 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 353 |
. . . 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 1827 |
. . 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 237 |
. 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 2742 |
. . . . 5
⊢ (𝑧 = 𝑞 → (𝑧 = [〈((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R ↔
𝑞 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
)) |
59 | 58 | anbi2d 632 |
. . . 4
⊢ (𝑧 = 𝑞 → (((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ ((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
60 | 59 | 4exbidv 1932 |
. . 3
⊢ (𝑧 = 𝑞 → (∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ ∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑞 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
61 | 60 | mo4 2566 |
. 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 237 |
1
⊢ ((𝐴 ∈ ((P
× P) / ~R ) ∧ 𝐵 ∈ ((P
× P) / ~R )) →
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝐴 = [〈𝑤, 𝑣〉] ~R ∧
𝐵 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
)) |