ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addnnnq0 GIF version

Theorem addnnnq0 7447
Description: Addition of nonnegative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.)
Assertion
Ref Expression
addnnnq0 (((𝐴 ∈ ω ∧ 𝐵N) ∧ (𝐶 ∈ ω ∧ 𝐷N)) → ([⟨𝐴, 𝐵⟩] ~Q0 +Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 )

Proof of Theorem addnnnq0
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opelxpi 4658 . . . 4 ((𝐴 ∈ ω ∧ 𝐵N) → ⟨𝐴, 𝐵⟩ ∈ (ω × N))
2 enq0ex 7437 . . . . 5 ~Q0 ∈ V
32ecelqsi 6588 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ω × N) → [⟨𝐴, 𝐵⟩] ~Q0 ∈ ((ω × N) / ~Q0 ))
41, 3syl 14 . . 3 ((𝐴 ∈ ω ∧ 𝐵N) → [⟨𝐴, 𝐵⟩] ~Q0 ∈ ((ω × N) / ~Q0 ))
5 opelxpi 4658 . . . 4 ((𝐶 ∈ ω ∧ 𝐷N) → ⟨𝐶, 𝐷⟩ ∈ (ω × N))
62ecelqsi 6588 . . . 4 (⟨𝐶, 𝐷⟩ ∈ (ω × N) → [⟨𝐶, 𝐷⟩] ~Q0 ∈ ((ω × N) / ~Q0 ))
75, 6syl 14 . . 3 ((𝐶 ∈ ω ∧ 𝐷N) → [⟨𝐶, 𝐷⟩] ~Q0 ∈ ((ω × N) / ~Q0 ))
84, 7anim12i 338 . 2 (((𝐴 ∈ ω ∧ 𝐵N) ∧ (𝐶 ∈ ω ∧ 𝐷N)) → ([⟨𝐴, 𝐵⟩] ~Q0 ∈ ((ω × N) / ~Q0 ) ∧ [⟨𝐶, 𝐷⟩] ~Q0 ∈ ((ω × N) / ~Q0 )))
9 eqid 2177 . . . 4 [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0
10 eqid 2177 . . . 4 [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0
119, 10pm3.2i 272 . . 3 ([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 )
12 eqid 2177 . . 3 [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0
13 opeq12 3780 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨𝑤, 𝑣⟩ = ⟨𝐴, 𝐵⟩)
1413eceq1d 6570 . . . . . . . 8 ((𝑤 = 𝐴𝑣 = 𝐵) → [⟨𝑤, 𝑣⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 )
1514eqeq2d 2189 . . . . . . 7 ((𝑤 = 𝐴𝑣 = 𝐵) → ([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ↔ [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 ))
1615anbi1d 465 . . . . . 6 ((𝑤 = 𝐴𝑣 = 𝐵) → (([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ↔ ([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 )))
17 simpl 109 . . . . . . . . . . 11 ((𝑤 = 𝐴𝑣 = 𝐵) → 𝑤 = 𝐴)
1817oveq1d 5889 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑤 ·o 𝐷) = (𝐴 ·o 𝐷))
19 simpr 110 . . . . . . . . . . 11 ((𝑤 = 𝐴𝑣 = 𝐵) → 𝑣 = 𝐵)
2019oveq1d 5889 . . . . . . . . . 10 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑣 ·o 𝐶) = (𝐵 ·o 𝐶))
2118, 20oveq12d 5892 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → ((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)) = ((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)))
2219oveq1d 5889 . . . . . . . . 9 ((𝑤 = 𝐴𝑣 = 𝐵) → (𝑣 ·o 𝐷) = (𝐵 ·o 𝐷))
2321, 22opeq12d 3786 . . . . . . . 8 ((𝑤 = 𝐴𝑣 = 𝐵) → ⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩ = ⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩)
2423eceq1d 6570 . . . . . . 7 ((𝑤 = 𝐴𝑣 = 𝐵) → [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 )
2524eqeq2d 2189 . . . . . 6 ((𝑤 = 𝐴𝑣 = 𝐵) → ([⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 ↔ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ))
2616, 25anbi12d 473 . . . . 5 ((𝑤 = 𝐴𝑣 = 𝐵) → ((([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 ) ↔ (([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 )))
2726spc2egv 2827 . . . 4 ((𝐴 ∈ ω ∧ 𝐵N) → ((([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → ∃𝑤𝑣(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 )))
28 opeq12 3780 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → ⟨𝑢, 𝑡⟩ = ⟨𝐶, 𝐷⟩)
2928eceq1d 6570 . . . . . . . . 9 ((𝑢 = 𝐶𝑡 = 𝐷) → [⟨𝑢, 𝑡⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 )
3029eqeq2d 2189 . . . . . . . 8 ((𝑢 = 𝐶𝑡 = 𝐷) → ([⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ↔ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ))
3130anbi2d 464 . . . . . . 7 ((𝑢 = 𝐶𝑡 = 𝐷) → (([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ↔ ([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 )))
32 simpr 110 . . . . . . . . . . . 12 ((𝑢 = 𝐶𝑡 = 𝐷) → 𝑡 = 𝐷)
3332oveq2d 5890 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑤 ·o 𝑡) = (𝑤 ·o 𝐷))
34 simpl 109 . . . . . . . . . . . 12 ((𝑢 = 𝐶𝑡 = 𝐷) → 𝑢 = 𝐶)
3534oveq2d 5890 . . . . . . . . . . 11 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑣 ·o 𝑢) = (𝑣 ·o 𝐶))
3633, 35oveq12d 5892 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → ((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)) = ((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)))
3732oveq2d 5890 . . . . . . . . . 10 ((𝑢 = 𝐶𝑡 = 𝐷) → (𝑣 ·o 𝑡) = (𝑣 ·o 𝐷))
3836, 37opeq12d 3786 . . . . . . . . 9 ((𝑢 = 𝐶𝑡 = 𝐷) → ⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩ = ⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩)
3938eceq1d 6570 . . . . . . . 8 ((𝑢 = 𝐶𝑡 = 𝐷) → [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 )
4039eqeq2d 2189 . . . . . . 7 ((𝑢 = 𝐶𝑡 = 𝐷) → ([⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ↔ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 ))
4131, 40anbi12d 473 . . . . . 6 ((𝑢 = 𝐶𝑡 = 𝐷) → ((([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ) ↔ (([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 )))
4241spc2egv 2827 . . . . 5 ((𝐶 ∈ ω ∧ 𝐷N) → ((([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 ) → ∃𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 )))
43422eximdv 1882 . . . 4 ((𝐶 ∈ ω ∧ 𝐷N) → (∃𝑤𝑣(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝐷) +o (𝑣 ·o 𝐶)), (𝑣 ·o 𝐷)⟩] ~Q0 ) → ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 )))
4427, 43sylan9 409 . . 3 (((𝐴 ∈ ω ∧ 𝐵N) ∧ (𝐶 ∈ ω ∧ 𝐷N)) → ((([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝐴, 𝐵⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝐶, 𝐷⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 )))
4511, 12, 44mp2ani 432 . 2 (((𝐴 ∈ ω ∧ 𝐵N) ∧ (𝐶 ∈ ω ∧ 𝐷N)) → ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ))
46 ecexg 6538 . . . 4 ( ~Q0 ∈ V → [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ∈ V)
472, 46ax-mp 5 . . 3 [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ∈ V
48 simp1 997 . . . . . . . 8 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → 𝑥 = [⟨𝐴, 𝐵⟩] ~Q0 )
4948eqeq1d 2186 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → (𝑥 = [⟨𝑤, 𝑣⟩] ~Q0 ↔ [⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ))
50 simp2 998 . . . . . . . 8 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → 𝑦 = [⟨𝐶, 𝐷⟩] ~Q0 )
5150eqeq1d 2186 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → (𝑦 = [⟨𝑢, 𝑡⟩] ~Q0 ↔ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ))
5249, 51anbi12d 473 . . . . . 6 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → ((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑡⟩] ~Q0 ) ↔ ([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 )))
53 simp3 999 . . . . . . 7 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → 𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 )
5453eqeq1d 2186 . . . . . 6 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → (𝑧 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ↔ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ))
5552, 54anbi12d 473 . . . . 5 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → (((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ) ↔ (([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 )))
56554exbidv 1870 . . . 4 ((𝑥 = [⟨𝐴, 𝐵⟩] ~Q0𝑦 = [⟨𝐶, 𝐷⟩] ~Q0𝑧 = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ) → (∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ) ↔ ∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 )))
57 addnq0mo 7445 . . . 4 ((𝑥 ∈ ((ω × N) / ~Q0 ) ∧ 𝑦 ∈ ((ω × N) / ~Q0 )) → ∃*𝑧𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ))
58 dfplq0qs 7428 . . . 4 +Q0 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ ((ω × N) / ~Q0 ) ∧ 𝑦 ∈ ((ω × N) / ~Q0 )) ∧ ∃𝑤𝑣𝑢𝑡((𝑥 = [⟨𝑤, 𝑣⟩] ~Q0𝑦 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ 𝑧 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ))}
5956, 57, 58ovig 5995 . . 3 (([⟨𝐴, 𝐵⟩] ~Q0 ∈ ((ω × N) / ~Q0 ) ∧ [⟨𝐶, 𝐷⟩] ~Q0 ∈ ((ω × N) / ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ∈ V) → (∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ) → ([⟨𝐴, 𝐵⟩] ~Q0 +Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ))
6047, 59mp3an3 1326 . 2 (([⟨𝐴, 𝐵⟩] ~Q0 ∈ ((ω × N) / ~Q0 ) ∧ [⟨𝐶, 𝐷⟩] ~Q0 ∈ ((ω × N) / ~Q0 )) → (∃𝑤𝑣𝑢𝑡(([⟨𝐴, 𝐵⟩] ~Q0 = [⟨𝑤, 𝑣⟩] ~Q0 ∧ [⟨𝐶, 𝐷⟩] ~Q0 = [⟨𝑢, 𝑡⟩] ~Q0 ) ∧ [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 = [⟨((𝑤 ·o 𝑡) +o (𝑣 ·o 𝑢)), (𝑣 ·o 𝑡)⟩] ~Q0 ) → ([⟨𝐴, 𝐵⟩] ~Q0 +Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 ))
618, 45, 60sylc 62 1 (((𝐴 ∈ ω ∧ 𝐵N) ∧ (𝐶 ∈ ω ∧ 𝐷N)) → ([⟨𝐴, 𝐵⟩] ~Q0 +Q0 [⟨𝐶, 𝐷⟩] ~Q0 ) = [⟨((𝐴 ·o 𝐷) +o (𝐵 ·o 𝐶)), (𝐵 ·o 𝐷)⟩] ~Q0 )
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978   = wceq 1353  wex 1492  wcel 2148  Vcvv 2737  cop 3595  ωcom 4589   × cxp 4624  (class class class)co 5874   +o coa 6413   ·o comu 6414  [cec 6532   / cqs 6533  Ncnpi 7270   ~Q0 ceq0 7284   +Q0 cplq0 7287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-id 4293  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-oadd 6420  df-omul 6421  df-er 6534  df-ec 6536  df-qs 6540  df-ni 7302  df-mi 7304  df-enq0 7422  df-nq0 7423  df-plq0 7425
This theorem is referenced by:  addclnq0  7449  nqpnq0nq  7451  nqnq0a  7452  nq0a0  7455  nnanq0  7456  distrnq0  7457  addassnq0  7460
  Copyright terms: Public domain W3C validator