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

Theorem mulcomprg 7040
Description: Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
Assertion
Ref Expression
mulcomprg ((𝐴P𝐵P) → (𝐴 ·P 𝐵) = (𝐵 ·P 𝐴))

Proof of Theorem mulcomprg
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prop 6935 . . . . . . . . 9 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
2 elprnql 6941 . . . . . . . . 9 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑧 ∈ (1st𝐵)) → 𝑧Q)
31, 2sylan 277 . . . . . . . 8 ((𝐵P𝑧 ∈ (1st𝐵)) → 𝑧Q)
4 prop 6935 . . . . . . . . . . . . 13 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
5 elprnql 6941 . . . . . . . . . . . . 13 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑦 ∈ (1st𝐴)) → 𝑦Q)
64, 5sylan 277 . . . . . . . . . . . 12 ((𝐴P𝑦 ∈ (1st𝐴)) → 𝑦Q)
7 mulcomnqg 6843 . . . . . . . . . . . . 13 ((𝑧Q𝑦Q) → (𝑧 ·Q 𝑦) = (𝑦 ·Q 𝑧))
87eqeq2d 2094 . . . . . . . . . . . 12 ((𝑧Q𝑦Q) → (𝑥 = (𝑧 ·Q 𝑦) ↔ 𝑥 = (𝑦 ·Q 𝑧)))
96, 8sylan2 280 . . . . . . . . . . 11 ((𝑧Q ∧ (𝐴P𝑦 ∈ (1st𝐴))) → (𝑥 = (𝑧 ·Q 𝑦) ↔ 𝑥 = (𝑦 ·Q 𝑧)))
109anassrs 392 . . . . . . . . . 10 (((𝑧Q𝐴P) ∧ 𝑦 ∈ (1st𝐴)) → (𝑥 = (𝑧 ·Q 𝑦) ↔ 𝑥 = (𝑦 ·Q 𝑧)))
1110rexbidva 2371 . . . . . . . . 9 ((𝑧Q𝐴P) → (∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (1st𝐴)𝑥 = (𝑦 ·Q 𝑧)))
1211ancoms 264 . . . . . . . 8 ((𝐴P𝑧Q) → (∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (1st𝐴)𝑥 = (𝑦 ·Q 𝑧)))
133, 12sylan2 280 . . . . . . 7 ((𝐴P ∧ (𝐵P𝑧 ∈ (1st𝐵))) → (∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (1st𝐴)𝑥 = (𝑦 ·Q 𝑧)))
1413anassrs 392 . . . . . 6 (((𝐴P𝐵P) ∧ 𝑧 ∈ (1st𝐵)) → (∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (1st𝐴)𝑥 = (𝑦 ·Q 𝑧)))
1514rexbidva 2371 . . . . 5 ((𝐴P𝐵P) → (∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑦 ·Q 𝑧)))
16 rexcom 2524 . . . . 5 (∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑦 ·Q 𝑧) ↔ ∃𝑦 ∈ (1st𝐴)∃𝑧 ∈ (1st𝐵)𝑥 = (𝑦 ·Q 𝑧))
1715, 16syl6bb 194 . . . 4 ((𝐴P𝐵P) → (∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (1st𝐴)∃𝑧 ∈ (1st𝐵)𝑥 = (𝑦 ·Q 𝑧)))
1817rabbidv 2601 . . 3 ((𝐴P𝐵P) → {𝑥Q ∣ ∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦)} = {𝑥Q ∣ ∃𝑦 ∈ (1st𝐴)∃𝑧 ∈ (1st𝐵)𝑥 = (𝑦 ·Q 𝑧)})
19 elprnqu 6942 . . . . . . . . 9 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑧 ∈ (2nd𝐵)) → 𝑧Q)
201, 19sylan 277 . . . . . . . 8 ((𝐵P𝑧 ∈ (2nd𝐵)) → 𝑧Q)
21 elprnqu 6942 . . . . . . . . . . . . 13 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑦 ∈ (2nd𝐴)) → 𝑦Q)
224, 21sylan 277 . . . . . . . . . . . 12 ((𝐴P𝑦 ∈ (2nd𝐴)) → 𝑦Q)
2322, 8sylan2 280 . . . . . . . . . . 11 ((𝑧Q ∧ (𝐴P𝑦 ∈ (2nd𝐴))) → (𝑥 = (𝑧 ·Q 𝑦) ↔ 𝑥 = (𝑦 ·Q 𝑧)))
2423anassrs 392 . . . . . . . . . 10 (((𝑧Q𝐴P) ∧ 𝑦 ∈ (2nd𝐴)) → (𝑥 = (𝑧 ·Q 𝑦) ↔ 𝑥 = (𝑦 ·Q 𝑧)))
2524rexbidva 2371 . . . . . . . . 9 ((𝑧Q𝐴P) → (∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑦 ·Q 𝑧)))
2625ancoms 264 . . . . . . . 8 ((𝐴P𝑧Q) → (∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑦 ·Q 𝑧)))
2720, 26sylan2 280 . . . . . . 7 ((𝐴P ∧ (𝐵P𝑧 ∈ (2nd𝐵))) → (∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑦 ·Q 𝑧)))
2827anassrs 392 . . . . . 6 (((𝐴P𝐵P) ∧ 𝑧 ∈ (2nd𝐵)) → (∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑦 ·Q 𝑧)))
2928rexbidva 2371 . . . . 5 ((𝐴P𝐵P) → (∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑦 ·Q 𝑧)))
30 rexcom 2524 . . . . 5 (∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑦 ·Q 𝑧) ↔ ∃𝑦 ∈ (2nd𝐴)∃𝑧 ∈ (2nd𝐵)𝑥 = (𝑦 ·Q 𝑧))
3129, 30syl6bb 194 . . . 4 ((𝐴P𝐵P) → (∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦) ↔ ∃𝑦 ∈ (2nd𝐴)∃𝑧 ∈ (2nd𝐵)𝑥 = (𝑦 ·Q 𝑧)))
3231rabbidv 2601 . . 3 ((𝐴P𝐵P) → {𝑥Q ∣ ∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦)} = {𝑥Q ∣ ∃𝑦 ∈ (2nd𝐴)∃𝑧 ∈ (2nd𝐵)𝑥 = (𝑦 ·Q 𝑧)})
3318, 32opeq12d 3604 . 2 ((𝐴P𝐵P) → ⟨{𝑥Q ∣ ∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦)}, {𝑥Q ∣ ∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦)}⟩ = ⟨{𝑥Q ∣ ∃𝑦 ∈ (1st𝐴)∃𝑧 ∈ (1st𝐵)𝑥 = (𝑦 ·Q 𝑧)}, {𝑥Q ∣ ∃𝑦 ∈ (2nd𝐴)∃𝑧 ∈ (2nd𝐵)𝑥 = (𝑦 ·Q 𝑧)}⟩)
34 mpvlu 6999 . . 3 ((𝐵P𝐴P) → (𝐵 ·P 𝐴) = ⟨{𝑥Q ∣ ∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦)}, {𝑥Q ∣ ∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦)}⟩)
3534ancoms 264 . 2 ((𝐴P𝐵P) → (𝐵 ·P 𝐴) = ⟨{𝑥Q ∣ ∃𝑧 ∈ (1st𝐵)∃𝑦 ∈ (1st𝐴)𝑥 = (𝑧 ·Q 𝑦)}, {𝑥Q ∣ ∃𝑧 ∈ (2nd𝐵)∃𝑦 ∈ (2nd𝐴)𝑥 = (𝑧 ·Q 𝑦)}⟩)
36 mpvlu 6999 . 2 ((𝐴P𝐵P) → (𝐴 ·P 𝐵) = ⟨{𝑥Q ∣ ∃𝑦 ∈ (1st𝐴)∃𝑧 ∈ (1st𝐵)𝑥 = (𝑦 ·Q 𝑧)}, {𝑥Q ∣ ∃𝑦 ∈ (2nd𝐴)∃𝑧 ∈ (2nd𝐵)𝑥 = (𝑦 ·Q 𝑧)}⟩)
3733, 35, 363eqtr4rd 2126 1 ((𝐴P𝐵P) → (𝐴 ·P 𝐵) = (𝐵 ·P 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wcel 1434  wrex 2354  {crab 2357  cop 3425  cfv 4967  (class class class)co 5589  1st c1st 5842  2nd c2nd 5843  Qcnq 6740   ·Q cmq 6743  Pcnp 6751   ·P cmp 6754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-coll 3919  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315  ax-iinf 4365
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-int 3663  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-tr 3902  df-id 4083  df-iord 4156  df-on 4158  df-suc 4161  df-iom 4368  df-xp 4405  df-rel 4406  df-cnv 4407  df-co 4408  df-dm 4409  df-rn 4410  df-res 4411  df-ima 4412  df-iota 4932  df-fun 4969  df-fn 4970  df-f 4971  df-f1 4972  df-fo 4973  df-f1o 4974  df-fv 4975  df-ov 5592  df-oprab 5593  df-mpt2 5594  df-1st 5844  df-2nd 5845  df-recs 6000  df-irdg 6065  df-oadd 6115  df-omul 6116  df-er 6220  df-ec 6222  df-qs 6226  df-ni 6764  df-mi 6766  df-mpq 6805  df-enq 6807  df-nqqs 6808  df-mqqs 6810  df-inp 6926  df-imp 6929
This theorem is referenced by:  ltmprr  7102  mulcmpblnrlemg  7187  mulcomsrg  7204  mulasssrg  7205  m1m1sr  7208  recexgt0sr  7220  mulgt0sr  7224  mulextsr1lem  7226  recidpirqlemcalc  7295
  Copyright terms: Public domain W3C validator