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

Theorem distrlem1pru 6416
Description: Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
Assertion
Ref Expression
distrlem1pru ((A P B P 𝐶 P) → (2nd ‘(A ·P (B +P 𝐶))) ⊆ (2nd ‘((A ·P B) +P (A ·P 𝐶))))

Proof of Theorem distrlem1pru
Dummy variables x y z w v f g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 addclpr 6386 . . . . 5 ((B P 𝐶 P) → (B +P 𝐶) P)
2 df-imp 6317 . . . . . 6 ·P = (y P, z P ↦ ⟨{f Qg Q Q (g (1sty) (1stz) f = (g ·Q ))}, {f Qg Q Q (g (2ndy) (2ndz) f = (g ·Q ))}⟩)
3 mulclnq 6229 . . . . . 6 ((g Q Q) → (g ·Q ) Q)
42, 3genpelvu 6361 . . . . 5 ((A P (B +P 𝐶) P) → (w (2nd ‘(A ·P (B +P 𝐶))) ↔ x (2ndA)v (2nd ‘(B +P 𝐶))w = (x ·Q v)))
51, 4sylan2 270 . . . 4 ((A P (B P 𝐶 P)) → (w (2nd ‘(A ·P (B +P 𝐶))) ↔ x (2ndA)v (2nd ‘(B +P 𝐶))w = (x ·Q v)))
653impb 1084 . . 3 ((A P B P 𝐶 P) → (w (2nd ‘(A ·P (B +P 𝐶))) ↔ x (2ndA)v (2nd ‘(B +P 𝐶))w = (x ·Q v)))
7 df-iplp 6316 . . . . . . . . . . 11 +P = (w P, x P ↦ ⟨{f Qg Q Q (g (1stw) (1stx) f = (g +Q ))}, {f Qg Q Q (g (2ndw) (2ndx) f = (g +Q ))}⟩)
8 addclnq 6228 . . . . . . . . . . 11 ((g Q Q) → (g +Q ) Q)
97, 8genpelvu 6361 . . . . . . . . . 10 ((B P 𝐶 P) → (v (2nd ‘(B +P 𝐶)) ↔ y (2ndB)z (2nd𝐶)v = (y +Q z)))
1093adant1 908 . . . . . . . . 9 ((A P B P 𝐶 P) → (v (2nd ‘(B +P 𝐶)) ↔ y (2ndB)z (2nd𝐶)v = (y +Q z)))
1110adantr 261 . . . . . . . 8 (((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) → (v (2nd ‘(B +P 𝐶)) ↔ y (2ndB)z (2nd𝐶)v = (y +Q z)))
12 prop 6323 . . . . . . . . . . . . . . . . 17 (A P → ⟨(1stA), (2ndA)⟩ P)
13 elprnqu 6330 . . . . . . . . . . . . . . . . 17 ((⟨(1stA), (2ndA)⟩ P x (2ndA)) → x Q)
1412, 13sylan 267 . . . . . . . . . . . . . . . 16 ((A P x (2ndA)) → x Q)
15143ad2antl1 1052 . . . . . . . . . . . . . . 15 (((A P B P 𝐶 P) x (2ndA)) → x Q)
1615adantrr 451 . . . . . . . . . . . . . 14 (((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) → x Q)
1716adantr 261 . . . . . . . . . . . . 13 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → x Q)
18 prop 6323 . . . . . . . . . . . . . . . . . 18 (B P → ⟨(1stB), (2ndB)⟩ P)
19 elprnqu 6330 . . . . . . . . . . . . . . . . . 18 ((⟨(1stB), (2ndB)⟩ P y (2ndB)) → y Q)
2018, 19sylan 267 . . . . . . . . . . . . . . . . 17 ((B P y (2ndB)) → y Q)
21 prop 6323 . . . . . . . . . . . . . . . . . 18 (𝐶 P → ⟨(1st𝐶), (2nd𝐶)⟩ P)
22 elprnqu 6330 . . . . . . . . . . . . . . . . . 18 ((⟨(1st𝐶), (2nd𝐶)⟩ P z (2nd𝐶)) → z Q)
2321, 22sylan 267 . . . . . . . . . . . . . . . . 17 ((𝐶 P z (2nd𝐶)) → z Q)
2420, 23anim12i 321 . . . . . . . . . . . . . . . 16 (((B P y (2ndB)) (𝐶 P z (2nd𝐶))) → (y Q z Q))
2524an4s 509 . . . . . . . . . . . . . . 15 (((B P 𝐶 P) (y (2ndB) z (2nd𝐶))) → (y Q z Q))
26253adantl1 1046 . . . . . . . . . . . . . 14 (((A P B P 𝐶 P) (y (2ndB) z (2nd𝐶))) → (y Q z Q))
2726ad2ant2r 466 . . . . . . . . . . . . 13 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (y Q z Q))
28 3anass 875 . . . . . . . . . . . . 13 ((x Q y Q z Q) ↔ (x Q (y Q z Q)))
2917, 27, 28sylanbrc 396 . . . . . . . . . . . 12 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (x Q y Q z Q))
30 simprr 472 . . . . . . . . . . . . 13 (((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) → w = (x ·Q v))
31 simpr 103 . . . . . . . . . . . . 13 (((y (2ndB) z (2nd𝐶)) v = (y +Q z)) → v = (y +Q z))
3230, 31anim12i 321 . . . . . . . . . . . 12 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (w = (x ·Q v) v = (y +Q z)))
33 oveq2 5440 . . . . . . . . . . . . . . 15 (v = (y +Q z) → (x ·Q v) = (x ·Q (y +Q z)))
3433eqeq2d 2029 . . . . . . . . . . . . . 14 (v = (y +Q z) → (w = (x ·Q v) ↔ w = (x ·Q (y +Q z))))
3534biimpac 282 . . . . . . . . . . . . 13 ((w = (x ·Q v) v = (y +Q z)) → w = (x ·Q (y +Q z)))
36 distrnqg 6240 . . . . . . . . . . . . . 14 ((x Q y Q z Q) → (x ·Q (y +Q z)) = ((x ·Q y) +Q (x ·Q z)))
3736eqeq2d 2029 . . . . . . . . . . . . 13 ((x Q y Q z Q) → (w = (x ·Q (y +Q z)) ↔ w = ((x ·Q y) +Q (x ·Q z))))
3835, 37syl5ib 143 . . . . . . . . . . . 12 ((x Q y Q z Q) → ((w = (x ·Q v) v = (y +Q z)) → w = ((x ·Q y) +Q (x ·Q z))))
3929, 32, 38sylc 56 . . . . . . . . . . 11 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → w = ((x ·Q y) +Q (x ·Q z)))
40 mulclpr 6410 . . . . . . . . . . . . . 14 ((A P B P) → (A ·P B) P)
41403adant3 910 . . . . . . . . . . . . 13 ((A P B P 𝐶 P) → (A ·P B) P)
4241ad2antrr 460 . . . . . . . . . . . 12 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (A ·P B) P)
43 mulclpr 6410 . . . . . . . . . . . . . 14 ((A P 𝐶 P) → (A ·P 𝐶) P)
44433adant2 909 . . . . . . . . . . . . 13 ((A P B P 𝐶 P) → (A ·P 𝐶) P)
4544ad2antrr 460 . . . . . . . . . . . 12 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (A ·P 𝐶) P)
46 simpll 469 . . . . . . . . . . . . 13 (((y (2ndB) z (2nd𝐶)) v = (y +Q z)) → y (2ndB))
472, 3genppreclu 6363 . . . . . . . . . . . . . . . 16 ((A P B P) → ((x (2ndA) y (2ndB)) → (x ·Q y) (2nd ‘(A ·P B))))
48473adant3 910 . . . . . . . . . . . . . . 15 ((A P B P 𝐶 P) → ((x (2ndA) y (2ndB)) → (x ·Q y) (2nd ‘(A ·P B))))
4948impl 362 . . . . . . . . . . . . . 14 ((((A P B P 𝐶 P) x (2ndA)) y (2ndB)) → (x ·Q y) (2nd ‘(A ·P B)))
5049adantlrr 455 . . . . . . . . . . . . 13 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) y (2ndB)) → (x ·Q y) (2nd ‘(A ·P B)))
5146, 50sylan2 270 . . . . . . . . . . . 12 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (x ·Q y) (2nd ‘(A ·P B)))
52 simplr 470 . . . . . . . . . . . . 13 (((y (2ndB) z (2nd𝐶)) v = (y +Q z)) → z (2nd𝐶))
532, 3genppreclu 6363 . . . . . . . . . . . . . . . 16 ((A P 𝐶 P) → ((x (2ndA) z (2nd𝐶)) → (x ·Q z) (2nd ‘(A ·P 𝐶))))
54533adant2 909 . . . . . . . . . . . . . . 15 ((A P B P 𝐶 P) → ((x (2ndA) z (2nd𝐶)) → (x ·Q z) (2nd ‘(A ·P 𝐶))))
5554impl 362 . . . . . . . . . . . . . 14 ((((A P B P 𝐶 P) x (2ndA)) z (2nd𝐶)) → (x ·Q z) (2nd ‘(A ·P 𝐶)))
5655adantlrr 455 . . . . . . . . . . . . 13 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) z (2nd𝐶)) → (x ·Q z) (2nd ‘(A ·P 𝐶)))
5752, 56sylan2 270 . . . . . . . . . . . 12 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → (x ·Q z) (2nd ‘(A ·P 𝐶)))
587, 8genppreclu 6363 . . . . . . . . . . . . 13 (((A ·P B) P (A ·P 𝐶) P) → (((x ·Q y) (2nd ‘(A ·P B)) (x ·Q z) (2nd ‘(A ·P 𝐶))) → ((x ·Q y) +Q (x ·Q z)) (2nd ‘((A ·P B) +P (A ·P 𝐶)))))
5958imp 115 . . . . . . . . . . . 12 ((((A ·P B) P (A ·P 𝐶) P) ((x ·Q y) (2nd ‘(A ·P B)) (x ·Q z) (2nd ‘(A ·P 𝐶)))) → ((x ·Q y) +Q (x ·Q z)) (2nd ‘((A ·P B) +P (A ·P 𝐶))))
6042, 45, 51, 57, 59syl22anc 1120 . . . . . . . . . . 11 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → ((x ·Q y) +Q (x ·Q z)) (2nd ‘((A ·P B) +P (A ·P 𝐶))))
6139, 60eqeltrd 2092 . . . . . . . . . 10 ((((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) ((y (2ndB) z (2nd𝐶)) v = (y +Q z))) → w (2nd ‘((A ·P B) +P (A ·P 𝐶))))
6261exp32 347 . . . . . . . . 9 (((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) → ((y (2ndB) z (2nd𝐶)) → (v = (y +Q z) → w (2nd ‘((A ·P B) +P (A ·P 𝐶))))))
6362rexlimdvv 2413 . . . . . . . 8 (((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) → (y (2ndB)z (2nd𝐶)v = (y +Q z) → w (2nd ‘((A ·P B) +P (A ·P 𝐶)))))
6411, 63sylbid 139 . . . . . . 7 (((A P B P 𝐶 P) (x (2ndA) w = (x ·Q v))) → (v (2nd ‘(B +P 𝐶)) → w (2nd ‘((A ·P B) +P (A ·P 𝐶)))))
6564exp32 347 . . . . . 6 ((A P B P 𝐶 P) → (x (2ndA) → (w = (x ·Q v) → (v (2nd ‘(B +P 𝐶)) → w (2nd ‘((A ·P B) +P (A ·P 𝐶)))))))
6665com34 77 . . . . 5 ((A P B P 𝐶 P) → (x (2ndA) → (v (2nd ‘(B +P 𝐶)) → (w = (x ·Q v) → w (2nd ‘((A ·P B) +P (A ·P 𝐶)))))))
6766impd 242 . . . 4 ((A P B P 𝐶 P) → ((x (2ndA) v (2nd ‘(B +P 𝐶))) → (w = (x ·Q v) → w (2nd ‘((A ·P B) +P (A ·P 𝐶))))))
6867rexlimdvv 2413 . . 3 ((A P B P 𝐶 P) → (x (2ndA)v (2nd ‘(B +P 𝐶))w = (x ·Q v) → w (2nd ‘((A ·P B) +P (A ·P 𝐶)))))
696, 68sylbid 139 . 2 ((A P B P 𝐶 P) → (w (2nd ‘(A ·P (B +P 𝐶))) → w (2nd ‘((A ·P B) +P (A ·P 𝐶)))))
7069ssrdv 2924 1 ((A P B P 𝐶 P) → (2nd ‘(A ·P (B +P 𝐶))) ⊆ (2nd ‘((A ·P B) +P (A ·P 𝐶))))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 871   = wceq 1226   wcel 1370  wrex 2281  wss 2890  cop 3349  cfv 4825  (class class class)co 5432  1st c1st 5684  2nd c2nd 5685  Qcnq 6134   +Q cplq 6136   ·Q cmq 6137  Pcnp 6145   +P cpp 6147   ·P cmp 6148
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-coll 3842  ax-sep 3845  ax-nul 3853  ax-pow 3897  ax-pr 3914  ax-un 4116  ax-setind 4200  ax-iinf 4234
This theorem depends on definitions:  df-bi 110  df-dc 731  df-3or 872  df-3an 873  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ne 2184  df-ral 2285  df-rex 2286  df-reu 2287  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-int 3586  df-iun 3629  df-br 3735  df-opab 3789  df-mpt 3790  df-tr 3825  df-eprel 3996  df-id 4000  df-po 4003  df-iso 4004  df-iord 4048  df-on 4050  df-suc 4053  df-iom 4237  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-fo 4831  df-f1o 4832  df-fv 4833  df-ov 5435  df-oprab 5436  df-mpt2 5437  df-1st 5686  df-2nd 5687  df-recs 5838  df-irdg 5874  df-1o 5912  df-2o 5913  df-oadd 5916  df-omul 5917  df-er 6013  df-ec 6015  df-qs 6019  df-ni 6158  df-pli 6159  df-mi 6160  df-lti 6161  df-plpq 6197  df-mpq 6198  df-enq 6200  df-nqqs 6201  df-plqqs 6202  df-mqqs 6203  df-1nqqs 6204  df-rq 6205  df-ltnqqs 6206  df-enq0 6273  df-nq0 6274  df-0nq0 6275  df-plq0 6276  df-mq0 6277  df-inp 6314  df-iplp 6316  df-imp 6317
This theorem is referenced by:  distrprg  6421
  Copyright terms: Public domain W3C validator