MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulsrpr Structured version   Visualization version   GIF version

Theorem mulsrpr 9935
Description: Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
Assertion
Ref Expression
mulsrpr (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R ·R [⟨𝐶, 𝐷⟩] ~R ) = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R )

Proof of Theorem mulsrpr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opelxpi 5182 . . . 4 ((𝐴P𝐵P) → ⟨𝐴, 𝐵⟩ ∈ (P × P))
2 enrex 9926 . . . . 5 ~R ∈ V
32ecelqsi 7846 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (P × P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
41, 3syl 17 . . 3 ((𝐴P𝐵P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
5 opelxpi 5182 . . . 4 ((𝐶P𝐷P) → ⟨𝐶, 𝐷⟩ ∈ (P × P))
62ecelqsi 7846 . . . 4 (⟨𝐶, 𝐷⟩ ∈ (P × P) → [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ))
75, 6syl 17 . . 3 ((𝐶P𝐷P) → [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ))
84, 7anim12i 589 . 2 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R )))
9 eqid 2651 . . . 4 [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R
10 eqid 2651 . . . 4 [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R
119, 10pm3.2i 470 . . 3 ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
12 eqid 2651 . . 3 [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R
13 opeq12 4435 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨𝑤, 𝑣⟩ = ⟨𝐴, 𝐵⟩)
1413eceq1d 7826 . . . . . . . 8 ((𝑤 = 𝐴𝑣 = 𝐵) → [⟨𝑤, 𝑣⟩] ~R = [⟨𝐴, 𝐵⟩] ~R )
1514eqeq2d 2661 . . . . . . 7 ((𝑤 = 𝐴𝑣 = 𝐵) → ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ))
1615anbi1d 741 . . . . . 6 ((𝑤 = 𝐴𝑣 = 𝐵) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
17 simpl 472 . . . . . . . . . . 11 ((𝑤 = 𝐴𝑣 = 𝐵) → 𝑤 = 𝐴)
1817oveq1d 6705 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑤 ·P 𝐶) = (𝐴 ·P 𝐶))
19 simpr 476 . . . . . . . . . . 11 ((𝑤 = 𝐴𝑣 = 𝐵) → 𝑣 = 𝐵)
2019oveq1d 6705 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑣 ·P 𝐷) = (𝐵 ·P 𝐷))
2118, 20oveq12d 6708 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → ((𝑤 ·P 𝐶) +P (𝑣 ·P 𝐷)) = ((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)))
2217oveq1d 6705 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑤 ·P 𝐷) = (𝐴 ·P 𝐷))
2319oveq1d 6705 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑣 ·P 𝐶) = (𝐵 ·P 𝐶))
2422, 23oveq12d 6708 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → ((𝑤 ·P 𝐷) +P (𝑣 ·P 𝐶)) = ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶)))
2521, 24opeq12d 4441 . . . . . . . 8 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨((𝑤 ·P 𝐶) +P (𝑣 ·P 𝐷)), ((𝑤 ·P 𝐷) +P (𝑣 ·P 𝐶))⟩ = ⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩)
2625eceq1d 7826 . . . . . . 7 ((𝑤 = 𝐴𝑣 = 𝐵) → [⟨((𝑤 ·P 𝐶) +P (𝑣 ·P 𝐷)), ((𝑤 ·P 𝐷) +P (𝑣 ·P 𝐶))⟩] ~R = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R )
2726eqeq2d 2661 . . . . . 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 ))
2816, 27anbi12d 747 . . . . 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 )))
2928spc2egv 3326 . . . 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 4435 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → ⟨𝑢, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
3130eceq1d 7826 . . . . . . . . 9 ((𝑢 = 𝐶𝑡 = 𝐷) → [⟨𝑢, 𝑡⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
3231eqeq2d 2661 . . . . . . . 8 ((𝑢 = 𝐶𝑡 = 𝐷) → ([⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ))
3332anbi2d 740 . . . . . . 7 ((𝑢 = 𝐶𝑡 = 𝐷) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
34 simpl 472 . . . . . . . . . . . 12 ((𝑢 = 𝐶𝑡 = 𝐷) → 𝑢 = 𝐶)
3534oveq2d 6706 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑤 ·P 𝑢) = (𝑤 ·P 𝐶))
36 simpr 476 . . . . . . . . . . . 12 ((𝑢 = 𝐶𝑡 = 𝐷) → 𝑡 = 𝐷)
3736oveq2d 6706 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑣 ·P 𝑡) = (𝑣 ·P 𝐷))
3835, 37oveq12d 6708 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → ((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)) = ((𝑤 ·P 𝐶) +P (𝑣 ·P 𝐷)))
3936oveq2d 6706 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑤 ·P 𝑡) = (𝑤 ·P 𝐷))
4034oveq2d 6706 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑣 ·P 𝑢) = (𝑣 ·P 𝐶))
4139, 40oveq12d 6708 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢)) = ((𝑤 ·P 𝐷) +P (𝑣 ·P 𝐶)))
4238, 41opeq12d 4441 . . . . . . . . 9 ((𝑢 = 𝐶𝑡 = 𝐷) → ⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩ = ⟨((𝑤 ·P 𝐶) +P (𝑣 ·P 𝐷)), ((𝑤 ·P 𝐷) +P (𝑣 ·P 𝐶))⟩)
4342eceq1d 7826 . . . . . . . 8 ((𝑢 = 𝐶𝑡 = 𝐷) → [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩] ~R = [⟨((𝑤 ·P 𝐶) +P (𝑣 ·P 𝐷)), ((𝑤 ·P 𝐷) +P (𝑣 ·P 𝐶))⟩] ~R )
4443eqeq2d 2661 . . . . . . 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 ))
4533, 44anbi12d 747 . . . . . 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 )))
4645spc2egv 3326 . . . . 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 )))
47462eximdv 1888 . . . 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 )))
4829, 47sylan9 690 . . 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 )))
4911, 12, 48mp2ani 714 . 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 7791 . . . 4 ( ~R ∈ V → [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ∈ V)
512, 50ax-mp 5 . . 3 [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ∈ V
52 simp1 1081 . . . . . . . 8 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ) → 𝑥 = [⟨𝐴, 𝐵⟩] ~R )
5352eqeq1d 2653 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ) → (𝑥 = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ))
54 simp2 1082 . . . . . . . 8 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ) → 𝑦 = [⟨𝐶, 𝐷⟩] ~R )
5554eqeq1d 2653 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ) → (𝑦 = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ))
5653, 55anbi12d 747 . . . . . 6 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ) → ((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R )))
57 simp3 1083 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R ) → 𝑧 = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R )
5857eqeq1d 2653 . . . . . 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 ))
5956, 58anbi12d 747 . . . . 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 )))
60594exbidv 1894 . . . 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 9933 . . . 4 ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) → ∃*𝑧𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩] ~R ))
62 df-mr 9918 . . . . 5 ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩] ~R ))}
63 df-nr 9916 . . . . . . . . 9 R = ((P × P) / ~R )
6463eleq2i 2722 . . . . . . . 8 (𝑥R𝑥 ∈ ((P × P) / ~R ))
6563eleq2i 2722 . . . . . . . 8 (𝑦R𝑦 ∈ ((P × P) / ~R ))
6664, 65anbi12i 733 . . . . . . 7 ((𝑥R𝑦R) ↔ (𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )))
6766anbi1i 731 . . . . . 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 )))
6867oprabbii 6752 . . . . 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 ))}
6962, 68eqtri 2673 . . . 4 ·R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨((𝑤 ·P 𝑢) +P (𝑣 ·P 𝑡)), ((𝑤 ·P 𝑡) +P (𝑣 ·P 𝑢))⟩] ~R ))}
7060, 61, 69ovig 6824 . . 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 ))
7151, 70mp3an3 1453 . 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 ))
728, 49, 71sylc 65 1 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R ·R [⟨𝐶, 𝐷⟩] ~R ) = [⟨((𝐴 ·P 𝐶) +P (𝐵 ·P 𝐷)), ((𝐴 ·P 𝐷) +P (𝐵 ·P 𝐶))⟩] ~R )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231  cop 4216   × cxp 5141  (class class class)co 6690  {coprab 6691  [cec 7785   / cqs 7786  Pcnp 9719   +P cpp 9721   ·P cmp 9722   ~R cer 9724  Rcnr 9725   ·R cmr 9730
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-omul 7610  df-er 7787  df-ec 7789  df-qs 7793  df-ni 9732  df-pli 9733  df-mi 9734  df-lti 9735  df-plpq 9768  df-mpq 9769  df-ltpq 9770  df-enq 9771  df-nq 9772  df-erq 9773  df-plq 9774  df-mq 9775  df-1nq 9776  df-rq 9777  df-ltnq 9778  df-np 9841  df-plp 9843  df-mp 9844  df-ltp 9845  df-enr 9915  df-nr 9916  df-mr 9918
This theorem is referenced by:  mulclsr  9943  mulcomsr  9948  mulasssr  9949  distrsr  9950  m1m1sr  9952  1idsr  9957  00sr  9958  recexsrlem  9962  mulgt0sr  9964
  Copyright terms: Public domain W3C validator