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

Theorem addpqnq 10082
 Description: Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 26-Dec-2014.) (New usage is discouraged.)
Assertion
Ref Expression
addpqnq ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = ([Q]‘(𝐴 +pQ 𝐵)))

Proof of Theorem addpqnq
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-plq 10058 . . . . 5 +Q = (([Q] ∘ +pQ ) ↾ (Q × Q))
21fveq1i 6438 . . . 4 ( +Q ‘⟨𝐴, 𝐵⟩) = ((([Q] ∘ +pQ ) ↾ (Q × Q))‘⟨𝐴, 𝐵⟩)
32a1i 11 . . 3 ((𝐴Q𝐵Q) → ( +Q ‘⟨𝐴, 𝐵⟩) = ((([Q] ∘ +pQ ) ↾ (Q × Q))‘⟨𝐴, 𝐵⟩))
4 opelxpi 5383 . . . 4 ((𝐴Q𝐵Q) → ⟨𝐴, 𝐵⟩ ∈ (Q × Q))
5 fvres 6456 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (Q × Q) → ((([Q] ∘ +pQ ) ↾ (Q × Q))‘⟨𝐴, 𝐵⟩) = (([Q] ∘ +pQ )‘⟨𝐴, 𝐵⟩))
64, 5syl 17 . . 3 ((𝐴Q𝐵Q) → ((([Q] ∘ +pQ ) ↾ (Q × Q))‘⟨𝐴, 𝐵⟩) = (([Q] ∘ +pQ )‘⟨𝐴, 𝐵⟩))
7 df-plpq 10052 . . . . 5 +pQ = (𝑥 ∈ (N × N), 𝑦 ∈ (N × N) ↦ ⟨(((1st𝑥) ·N (2nd𝑦)) +N ((1st𝑦) ·N (2nd𝑥))), ((2nd𝑥) ·N (2nd𝑦))⟩)
8 opex 5155 . . . . 5 ⟨(((1st𝑥) ·N (2nd𝑦)) +N ((1st𝑦) ·N (2nd𝑥))), ((2nd𝑥) ·N (2nd𝑦))⟩ ∈ V
97, 8fnmpt2i 7507 . . . 4 +pQ Fn ((N × N) × (N × N))
10 elpqn 10069 . . . . 5 (𝐴Q𝐴 ∈ (N × N))
11 elpqn 10069 . . . . 5 (𝐵Q𝐵 ∈ (N × N))
12 opelxpi 5383 . . . . 5 ((𝐴 ∈ (N × N) ∧ 𝐵 ∈ (N × N)) → ⟨𝐴, 𝐵⟩ ∈ ((N × N) × (N × N)))
1310, 11, 12syl2an 589 . . . 4 ((𝐴Q𝐵Q) → ⟨𝐴, 𝐵⟩ ∈ ((N × N) × (N × N)))
14 fvco2 6524 . . . 4 (( +pQ Fn ((N × N) × (N × N)) ∧ ⟨𝐴, 𝐵⟩ ∈ ((N × N) × (N × N))) → (([Q] ∘ +pQ )‘⟨𝐴, 𝐵⟩) = ([Q]‘( +pQ ‘⟨𝐴, 𝐵⟩)))
159, 13, 14sylancr 581 . . 3 ((𝐴Q𝐵Q) → (([Q] ∘ +pQ )‘⟨𝐴, 𝐵⟩) = ([Q]‘( +pQ ‘⟨𝐴, 𝐵⟩)))
163, 6, 153eqtrd 2865 . 2 ((𝐴Q𝐵Q) → ( +Q ‘⟨𝐴, 𝐵⟩) = ([Q]‘( +pQ ‘⟨𝐴, 𝐵⟩)))
17 df-ov 6913 . 2 (𝐴 +Q 𝐵) = ( +Q ‘⟨𝐴, 𝐵⟩)
18 df-ov 6913 . . 3 (𝐴 +pQ 𝐵) = ( +pQ ‘⟨𝐴, 𝐵⟩)
1918fveq2i 6440 . 2 ([Q]‘(𝐴 +pQ 𝐵)) = ([Q]‘( +pQ ‘⟨𝐴, 𝐵⟩))
2016, 17, 193eqtr4g 2886 1 ((𝐴Q𝐵Q) → (𝐴 +Q 𝐵) = ([Q]‘(𝐴 +pQ 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1656   ∈ wcel 2164  ⟨cop 4405   × cxp 5344   ↾ cres 5348   ∘ ccom 5350   Fn wfn 6122  ‘cfv 6127  (class class class)co 6910  1st c1st 7431  2nd c2nd 7432  Ncnpi 9988   +N cpli 9989   ·N cmi 9990   +pQ cplpq 9992  Qcnq 9996  [Q]cerq 9998   +Q cplq 9999 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-fv 6135  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-1st 7433  df-2nd 7434  df-plpq 10052  df-nq 10056  df-plq 10058 This theorem is referenced by:  addclnq  10089  addcomnq  10095  adderpq  10100  addassnq  10102  distrnq  10105  ltanq  10115  1lt2nq  10117  prlem934  10177
 Copyright terms: Public domain W3C validator