| Step | Hyp | Ref
| Expression |
| 1 | | opelxpi 5722 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ 〈𝐴, 𝐵〉 ∈ (P
× P)) |
| 2 | | enrex 11107 |
. . . . 5
⊢
~R ∈ V |
| 3 | 2 | ecelqsi 8813 |
. . . 4
⊢
(〈𝐴, 𝐵〉 ∈ (P
× P) → [〈𝐴, 𝐵〉] ~R ∈
((P × P) / ~R
)) |
| 4 | 1, 3 | syl 17 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ [〈𝐴, 𝐵〉]
~R ∈ ((P × P)
/ ~R )) |
| 5 | | opelxpi 5722 |
. . . 4
⊢ ((𝐶 ∈ P ∧
𝐷 ∈ P)
→ 〈𝐶, 𝐷〉 ∈ (P
× P)) |
| 6 | 2 | ecelqsi 8813 |
. . . 4
⊢
(〈𝐶, 𝐷〉 ∈ (P
× P) → [〈𝐶, 𝐷〉] ~R ∈
((P × P) / ~R
)) |
| 7 | 5, 6 | syl 17 |
. . 3
⊢ ((𝐶 ∈ P ∧
𝐷 ∈ P)
→ [〈𝐶, 𝐷〉]
~R ∈ ((P × P)
/ ~R )) |
| 8 | 4, 7 | anim12i 613 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ([〈𝐴, 𝐵〉] ~R ∈
((P × P) / ~R
) ∧ [〈𝐶, 𝐷〉]
~R ∈ ((P × P)
/ ~R ))) |
| 9 | | eqid 2737 |
. . . 4
⊢
[〈𝐴, 𝐵〉]
~R = [〈𝐴, 𝐵〉]
~R |
| 10 | | eqid 2737 |
. . . 4
⊢
[〈𝐶, 𝐷〉]
~R = [〈𝐶, 𝐷〉]
~R |
| 11 | 9, 10 | pm3.2i 470 |
. . 3
⊢
([〈𝐴, 𝐵〉]
~R = [〈𝐴, 𝐵〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
) |
| 12 | | eqid 2737 |
. . 3
⊢
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉]
~R |
| 13 | | opeq12 4875 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 〈𝑤, 𝑣〉 = 〈𝐴, 𝐵〉) |
| 14 | 13 | eceq1d 8785 |
. . . . . . . 8
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → [〈𝑤, 𝑣〉] ~R =
[〈𝐴, 𝐵〉] ~R
) |
| 15 | 14 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ↔ [〈𝐴, 𝐵〉] ~R =
[〈𝐴, 𝐵〉] ~R
)) |
| 16 | 15 | anbi1d 631 |
. . . . . 6
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ↔
([〈𝐴, 𝐵〉]
~R = [〈𝐴, 𝐵〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
))) |
| 17 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 𝑤 = 𝐴) |
| 18 | 17 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑤 ·P 𝐶) = (𝐴 ·P 𝐶)) |
| 19 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 𝑣 = 𝐵) |
| 20 | 19 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑣 ·P 𝐷) = (𝐵 ·P 𝐷)) |
| 21 | 18, 20 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((𝑤 ·P 𝐶) +P
(𝑣
·P 𝐷)) = ((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷))) |
| 22 | 17 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑤 ·P 𝐷) = (𝐴 ·P 𝐷)) |
| 23 | 19 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → (𝑣 ·P 𝐶) = (𝐵 ·P 𝐶)) |
| 24 | 22, 23 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶)) = ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))) |
| 25 | 21, 24 | opeq12d 4881 |
. . . . . . . 8
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → 〈((𝑤 ·P 𝐶) +P
(𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉 = 〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉) |
| 26 | 25 | eceq1d 8785 |
. . . . . . 7
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → [〈((𝑤 ·P 𝐶) +P
(𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
) |
| 27 | 26 | eqeq2d 2748 |
. . . . . 6
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ([〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R ↔
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
)) |
| 28 | 16, 27 | anbi12d 632 |
. . . . 5
⊢ ((𝑤 = 𝐴 ∧ 𝑣 = 𝐵) → ((([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R )
↔ (([〈𝐴, 𝐵〉]
~R = [〈𝐴, 𝐵〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
))) |
| 29 | 28 | spc2egv 3599 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((([〈𝐴, 𝐵〉]
~R = [〈𝐴, 𝐵〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ ∃𝑤∃𝑣(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R
))) |
| 30 | | opeq12 4875 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 〈𝑢, 𝑡〉 = 〈𝐶, 𝐷〉) |
| 31 | 30 | eceq1d 8785 |
. . . . . . . . 9
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → [〈𝑢, 𝑡〉] ~R =
[〈𝐶, 𝐷〉] ~R
) |
| 32 | 31 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ([〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ↔ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
)) |
| 33 | 32 | anbi2d 630 |
. . . . . . 7
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ↔ ([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R
))) |
| 34 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 𝑢 = 𝐶) |
| 35 | 34 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑤 ·P 𝑢) = (𝑤 ·P 𝐶)) |
| 36 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 𝑡 = 𝐷) |
| 37 | 36 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑣 ·P 𝑡) = (𝑣 ·P 𝐷)) |
| 38 | 35, 37 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)) = ((𝑤 ·P 𝐶) +P
(𝑣
·P 𝐷))) |
| 39 | 36 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑤 ·P 𝑡) = (𝑤 ·P 𝐷)) |
| 40 | 34 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → (𝑣 ·P 𝑢) = (𝑣 ·P 𝐶)) |
| 41 | 39, 40 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢)) = ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))) |
| 42 | 38, 41 | opeq12d 4881 |
. . . . . . . . 9
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → 〈((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉 = 〈((𝑤 ·P 𝐶) +P
(𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉) |
| 43 | 42 | eceq1d 8785 |
. . . . . . . 8
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → [〈((𝑤 ·P 𝑢) +P
(𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R
) |
| 44 | 43 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ([〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R ↔
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R
)) |
| 45 | 33, 44 | anbi12d 632 |
. . . . . 6
⊢ ((𝑢 = 𝐶 ∧ 𝑡 = 𝐷) → ((([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ (([〈𝐴, 𝐵〉]
~R = [〈𝑤, 𝑣〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R
))) |
| 46 | 45 | spc2egv 3599 |
. . . . 5
⊢ ((𝐶 ∈ P ∧
𝐷 ∈ P)
→ ((([〈𝐴, 𝐵〉]
~R = [〈𝑤, 𝑣〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R )
→ ∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
| 47 | 46 | 2eximdv 1919 |
. . . 4
⊢ ((𝐶 ∈ P ∧
𝐷 ∈ P)
→ (∃𝑤∃𝑣(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝐶) +P (𝑣
·P 𝐷)), ((𝑤 ·P 𝐷) +P
(𝑣
·P 𝐶))〉] ~R )
→ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
| 48 | 29, 47 | sylan9 507 |
. . 3
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ((([〈𝐴, 𝐵〉] ~R =
[〈𝐴, 𝐵〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝐶, 𝐷〉] ~R ) ∧
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
| 49 | 11, 12, 48 | mp2ani 698 |
. 2
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
)) |
| 50 | | ecexg 8749 |
. . . 4
⊢ (
~R ∈ V → [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R ∈
V) |
| 51 | 2, 50 | ax-mp 5 |
. . 3
⊢
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R ∈
V |
| 52 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ 𝑥 = [〈𝐴, 𝐵〉] ~R
) |
| 53 | 52 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ (𝑥 = [〈𝑤, 𝑣〉] ~R ↔
[〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R )) |
| 54 | | simp2 1138 |
. . . . . . . 8
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ 𝑦 = [〈𝐶, 𝐷〉] ~R
) |
| 55 | 54 | eqeq1d 2739 |
. . . . . . 7
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ (𝑦 = [〈𝑢, 𝑡〉] ~R ↔
[〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R )) |
| 56 | 53, 55 | anbi12d 632 |
. . . . . 6
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ ((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ↔
([〈𝐴, 𝐵〉]
~R = [〈𝑤, 𝑣〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ))) |
| 57 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ 𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
) |
| 58 | 57 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ (𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R ↔
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
)) |
| 59 | 56, 58 | anbi12d 632 |
. . . . 5
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ (((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ (([〈𝐴, 𝐵〉]
~R = [〈𝑤, 𝑣〉] ~R ∧
[〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
| 60 | 59 | 4exbidv 1926 |
. . . 4
⊢ ((𝑥 = [〈𝐴, 𝐵〉] ~R ∧
𝑦 = [〈𝐶, 𝐷〉] ~R ∧
𝑧 = [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R )
→ (∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
↔ ∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
| 61 | | mulsrmo 11114 |
. . . 4
⊢ ((𝑥 ∈ ((P
× P) / ~R ) ∧ 𝑦 ∈ ((P
× P) / ~R )) →
∃*𝑧∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
)) |
| 62 | | df-mr 11098 |
. . . . 5
⊢
·R = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))} |
| 63 | | df-nr 11096 |
. . . . . . . . 9
⊢
R = ((P × P) /
~R ) |
| 64 | 63 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑥 ∈ R ↔
𝑥 ∈ ((P
× P) / ~R
)) |
| 65 | 63 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑦 ∈ R ↔
𝑦 ∈ ((P
× P) / ~R
)) |
| 66 | 64, 65 | anbi12i 628 |
. . . . . . 7
⊢ ((𝑥 ∈ R ∧
𝑦 ∈ R)
↔ (𝑥 ∈
((P × P) / ~R
) ∧ 𝑦 ∈
((P × P) / ~R
))) |
| 67 | 66 | anbi1i 624 |
. . . . . 6
⊢ (((𝑥 ∈ R ∧
𝑦 ∈ R)
∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R ))
↔ ((𝑥 ∈
((P × P) / ~R
) ∧ 𝑦 ∈
((P × P) / ~R
)) ∧ ∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))) |
| 68 | 67 | oprabbii 7500 |
. . . . 5
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ R ∧ 𝑦 ∈ R) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R ))} =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((P ×
P) / ~R ) ∧ 𝑦 ∈ ((P
× P) / ~R )) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))} |
| 69 | 62, 68 | eqtri 2765 |
. . . 4
⊢
·R = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ ((P ×
P) / ~R ) ∧ 𝑦 ∈ ((P
× P) / ~R )) ∧
∃𝑤∃𝑣∃𝑢∃𝑡((𝑥 = [〈𝑤, 𝑣〉] ~R ∧
𝑦 = [〈𝑢, 𝑡〉] ~R ) ∧
𝑧 = [〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R
))} |
| 70 | 60, 61, 69 | ovig 7579 |
. . 3
⊢
(([〈𝐴, 𝐵〉]
~R ∈ ((P × P)
/ ~R ) ∧ [〈𝐶, 𝐷〉] ~R ∈
((P × P) / ~R
) ∧ [〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R ∈
V) → (∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
→ ([〈𝐴, 𝐵〉]
~R ·R [〈𝐶, 𝐷〉] ~R ) =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
)) |
| 71 | 51, 70 | mp3an3 1452 |
. 2
⊢
(([〈𝐴, 𝐵〉]
~R ∈ ((P × P)
/ ~R ) ∧ [〈𝐶, 𝐷〉] ~R ∈
((P × P) / ~R
)) → (∃𝑤∃𝑣∃𝑢∃𝑡(([〈𝐴, 𝐵〉] ~R =
[〈𝑤, 𝑣〉]
~R ∧ [〈𝐶, 𝐷〉] ~R =
[〈𝑢, 𝑡〉]
~R ) ∧ [〈((𝐴 ·P 𝐶) +P
(𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R =
[〈((𝑤
·P 𝑢) +P (𝑣
·P 𝑡)), ((𝑤 ·P 𝑡) +P
(𝑣
·P 𝑢))〉] ~R )
→ ([〈𝐴, 𝐵〉]
~R ·R [〈𝐶, 𝐷〉] ~R ) =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
)) |
| 72 | 8, 49, 71 | sylc 65 |
1
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝐶 ∈
P ∧ 𝐷
∈ P)) → ([〈𝐴, 𝐵〉] ~R
·R [〈𝐶, 𝐷〉] ~R ) =
[〈((𝐴
·P 𝐶) +P (𝐵
·P 𝐷)), ((𝐴 ·P 𝐷) +P
(𝐵
·P 𝐶))〉] ~R
) |