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

Theorem addsrpr 9841
Description: Addition 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
addsrpr (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )

Proof of Theorem addsrpr
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opelxpi 5113 . . . 4 ((𝐴P𝐵P) → ⟨𝐴, 𝐵⟩ ∈ (P × P))
2 enrex 9833 . . . . 5 ~R ∈ V
32ecelqsi 7749 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (P × P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
41, 3syl 17 . . 3 ((𝐴P𝐵P) → [⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ))
5 opelxpi 5113 . . . 4 ((𝐶P𝐷P) → ⟨𝐶, 𝐷⟩ ∈ (P × P))
62ecelqsi 7749 . . . 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 2626 . . . 4 [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R
10 eqid 2626 . . . 4 [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R
119, 10pm3.2i 471 . . 3 ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
12 eqid 2626 . . 3 [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R
13 opeq12 4377 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨𝑤, 𝑣⟩ = ⟨𝐴, 𝐵⟩)
1413eceq1d 7729 . . . . . . . 8 ((𝑤 = 𝐴𝑣 = 𝐵) → [⟨𝑤, 𝑣⟩] ~R = [⟨𝐴, 𝐵⟩] ~R )
1514eqeq2d 2636 . . . . . . 7 ((𝑤 = 𝐴𝑣 = 𝐵) → ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ))
1615anbi1d 740 . . . . . 6 ((𝑤 = 𝐴𝑣 = 𝐵) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
17 simpl 473 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → 𝑤 = 𝐴)
1817oveq1d 6620 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑤 +P 𝐶) = (𝐴 +P 𝐶))
19 simpr 477 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → 𝑣 = 𝐵)
2019oveq1d 6620 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑣 +P 𝐷) = (𝐵 +P 𝐷))
2118, 20opeq12d 4383 . . . . . . . 8 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩ = ⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩)
2221eceq1d 7729 . . . . . . 7 ((𝑤 = 𝐴𝑣 = 𝐵) → [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
2322eqeq2d 2636 . . . . . 6 ((𝑤 = 𝐴𝑣 = 𝐵) → ([⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
2416, 23anbi12d 746 . . . . 5 ((𝑤 = 𝐴𝑣 = 𝐵) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )))
2524spc2egv 3286 . . . 4 ((𝐴P𝐵P) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ∃𝑤𝑣(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )))
26 opeq12 4377 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → ⟨𝑢, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
2726eceq1d 7729 . . . . . . . . 9 ((𝑢 = 𝐶𝑡 = 𝐷) → [⟨𝑢, 𝑡⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )
2827eqeq2d 2636 . . . . . . . 8 ((𝑢 = 𝐶𝑡 = 𝐷) → ([⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ))
2928anbi2d 739 . . . . . . 7 ((𝑢 = 𝐶𝑡 = 𝐷) → (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R )))
30 simpl 473 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → 𝑢 = 𝐶)
3130oveq2d 6621 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑤 +P 𝑢) = (𝑤 +P 𝐶))
32 simpr 477 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → 𝑡 = 𝐷)
3332oveq2d 6621 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑣 +P 𝑡) = (𝑣 +P 𝐷))
3431, 33opeq12d 4383 . . . . . . . . 9 ((𝑢 = 𝐶𝑡 = 𝐷) → ⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩ = ⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩)
3534eceq1d 7729 . . . . . . . 8 ((𝑢 = 𝐶𝑡 = 𝐷) → [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )
3635eqeq2d 2636 . . . . . . 7 ((𝑢 = 𝐶𝑡 = 𝐷) → ([⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ))
3729, 36anbi12d 746 . . . . . 6 ((𝑢 = 𝐶𝑡 = 𝐷) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R )))
3837spc2egv 3286 . . . . 5 ((𝐶P𝐷P) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) → ∃𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
39382eximdv 1850 . . . 4 ((𝐶P𝐷P) → (∃𝑤𝑣(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝐶), (𝑣 +P 𝐷)⟩] ~R ) → ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
4025, 39sylan9 688 . . 3 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ((([⟨𝐴, 𝐵⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
4111, 12, 40mp2ani 713 . 2 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
42 ecexg 7692 . . . 4 ( ~R ∈ V → [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V)
432, 42ax-mp 5 . . 3 [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V
44 simp1 1059 . . . . . . . 8 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑥 = [⟨𝐴, 𝐵⟩] ~R )
4544eqeq1d 2628 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑥 = [⟨𝑤, 𝑣⟩] ~R ↔ [⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ))
46 simp2 1060 . . . . . . . 8 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑦 = [⟨𝐶, 𝐷⟩] ~R )
4746eqeq1d 2628 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑦 = [⟨𝑢, 𝑡⟩] ~R ↔ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ))
4845, 47anbi12d 746 . . . . . 6 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → ((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ↔ ([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R )))
49 simp3 1061 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → 𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
5049eqeq1d 2628 . . . . . 6 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ↔ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
5148, 50anbi12d 746 . . . . 5 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ (([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
52514exbidv 1856 . . . 4 ((𝑥 = [⟨𝐴, 𝐵⟩] ~R𝑦 = [⟨𝐶, 𝐷⟩] ~R𝑧 = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ) → (∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) ↔ ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
53 addsrmo 9839 . . . 4 ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) → ∃*𝑧𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))
54 df-plr 9824 . . . . 5 +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
55 df-nr 9823 . . . . . . . . 9 R = ((P × P) / ~R )
5655eleq2i 2696 . . . . . . . 8 (𝑥R𝑥 ∈ ((P × P) / ~R ))
5755eleq2i 2696 . . . . . . . 8 (𝑦R𝑦 ∈ ((P × P) / ~R ))
5856, 57anbi12i 732 . . . . . . 7 ((𝑥R𝑦R) ↔ (𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )))
5958anbi1i 730 . . . . . 6 (((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )) ↔ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R )))
6059oprabbii 6664 . . . . 5 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
6154, 60eqtri 2648 . . . 4 +R = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((P × P) / ~R ) ∧ 𝑦 ∈ ((P × P) / ~R )) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~R𝑦 = [⟨𝑢, 𝑡⟩] ~R ) ∧ 𝑧 = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ))}
6252, 53, 61ovig 6736 . . 3 (([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ∈ V) → (∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
6343, 62mp3an3 1410 . 2 (([⟨𝐴, 𝐵⟩] ~R ∈ ((P × P) / ~R ) ∧ [⟨𝐶, 𝐷⟩] ~R ∈ ((P × P) / ~R )) → (∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~R = [⟨𝑤, 𝑣⟩] ~R ∧ [⟨𝐶, 𝐷⟩] ~R = [⟨𝑢, 𝑡⟩] ~R ) ∧ [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R = [⟨(𝑤 +P 𝑢), (𝑣 +P 𝑡)⟩] ~R ) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R ))
648, 41, 63sylc 65 1 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R +R [⟨𝐶, 𝐷⟩] ~R ) = [⟨(𝐴 +P 𝐶), (𝐵 +P 𝐷)⟩] ~R )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1992  Vcvv 3191  cop 4159   × cxp 5077  (class class class)co 6605  {coprab 6606  [cec 7686   / cqs 7687  Pcnp 9626   +P cpp 9628   ~R cer 9631  Rcnr 9632   +R cplr 9636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-omul 7511  df-er 7688  df-ec 7690  df-qs 7694  df-ni 9639  df-pli 9640  df-mi 9641  df-lti 9642  df-plpq 9675  df-mpq 9676  df-ltpq 9677  df-enq 9678  df-nq 9679  df-erq 9680  df-plq 9681  df-mq 9682  df-1nq 9683  df-rq 9684  df-ltnq 9685  df-np 9748  df-plp 9750  df-ltp 9752  df-enr 9822  df-nr 9823  df-plr 9824
This theorem is referenced by:  addclsr  9849  addcomsr  9853  addasssr  9854  distrsr  9857  m1p1sr  9858  0idsr  9863  ltasr  9866
  Copyright terms: Public domain W3C validator