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

Theorem distrlem4prl 7574
Description: Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
Assertion
Ref Expression
distrlem4prl (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑓,𝐴   𝑥,𝐵,𝑦,𝑧,𝑓   𝑥,𝐶,𝑦,𝑧,𝑓

Proof of Theorem distrlem4prl
Dummy variables 𝑤 𝑣 𝑢 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltmnqg 7391 . . . . . . 7 ((𝑤Q𝑣Q𝑢Q) → (𝑤 <Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q (𝑢 ·Q 𝑣)))
21adantl 277 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q𝑢Q)) → (𝑤 <Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q (𝑢 ·Q 𝑣)))
3 simp1 997 . . . . . . 7 ((𝐴P𝐵P𝐶P) → 𝐴P)
4 simpll 527 . . . . . . 7 (((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶))) → 𝑥 ∈ (1st𝐴))
5 prop 7465 . . . . . . . 8 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
6 elprnql 7471 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (1st𝐴)) → 𝑥Q)
75, 6sylan 283 . . . . . . 7 ((𝐴P𝑥 ∈ (1st𝐴)) → 𝑥Q)
83, 4, 7syl2an 289 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑥Q)
9 simprl 529 . . . . . . 7 (((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶))) → 𝑓 ∈ (1st𝐴))
10 elprnql 7471 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (1st𝐴)) → 𝑓Q)
115, 10sylan 283 . . . . . . 7 ((𝐴P𝑓 ∈ (1st𝐴)) → 𝑓Q)
123, 9, 11syl2an 289 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑓Q)
13 simpl2 1001 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝐵P)
14 simprlr 538 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑦 ∈ (1st𝐵))
15 prop 7465 . . . . . . . 8 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
16 elprnql 7471 . . . . . . . 8 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑦 ∈ (1st𝐵)) → 𝑦Q)
1715, 16sylan 283 . . . . . . 7 ((𝐵P𝑦 ∈ (1st𝐵)) → 𝑦Q)
1813, 14, 17syl2anc 411 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑦Q)
19 mulcomnqg 7373 . . . . . . 7 ((𝑤Q𝑣Q) → (𝑤 ·Q 𝑣) = (𝑣 ·Q 𝑤))
2019adantl 277 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q)) → (𝑤 ·Q 𝑣) = (𝑣 ·Q 𝑤))
212, 8, 12, 18, 20caovord2d 6038 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 <Q 𝑓 ↔ (𝑥 ·Q 𝑦) <Q (𝑓 ·Q 𝑦)))
22 ltanqg 7390 . . . . . . 7 ((𝑤Q𝑣Q𝑢Q) → (𝑤 <Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q (𝑢 +Q 𝑣)))
2322adantl 277 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q𝑢Q)) → (𝑤 <Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q (𝑢 +Q 𝑣)))
24 mulclnq 7366 . . . . . . 7 ((𝑥Q𝑦Q) → (𝑥 ·Q 𝑦) ∈ Q)
258, 18, 24syl2anc 411 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q 𝑦) ∈ Q)
26 mulclnq 7366 . . . . . . 7 ((𝑓Q𝑦Q) → (𝑓 ·Q 𝑦) ∈ Q)
2712, 18, 26syl2anc 411 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q 𝑦) ∈ Q)
28 simpl3 1002 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝐶P)
29 simprrr 540 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑧 ∈ (1st𝐶))
30 prop 7465 . . . . . . . . 9 (𝐶P → ⟨(1st𝐶), (2nd𝐶)⟩ ∈ P)
31 elprnql 7471 . . . . . . . . 9 ((⟨(1st𝐶), (2nd𝐶)⟩ ∈ P𝑧 ∈ (1st𝐶)) → 𝑧Q)
3230, 31sylan 283 . . . . . . . 8 ((𝐶P𝑧 ∈ (1st𝐶)) → 𝑧Q)
3328, 29, 32syl2anc 411 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑧Q)
34 mulclnq 7366 . . . . . . 7 ((𝑓Q𝑧Q) → (𝑓 ·Q 𝑧) ∈ Q)
3512, 33, 34syl2anc 411 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q 𝑧) ∈ Q)
36 addcomnqg 7371 . . . . . . 7 ((𝑤Q𝑣Q) → (𝑤 +Q 𝑣) = (𝑣 +Q 𝑤))
3736adantl 277 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q)) → (𝑤 +Q 𝑣) = (𝑣 +Q 𝑤))
3823, 25, 27, 35, 37caovord2d 6038 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 ·Q 𝑦) <Q (𝑓 ·Q 𝑦) ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧))))
3921, 38bitrd 188 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 <Q 𝑓 ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧))))
40 simpl1 1000 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝐴P)
41 addclpr 7527 . . . . . . . 8 ((𝐵P𝐶P) → (𝐵 +P 𝐶) ∈ P)
42413adant1 1015 . . . . . . 7 ((𝐴P𝐵P𝐶P) → (𝐵 +P 𝐶) ∈ P)
4342adantr 276 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝐵 +P 𝐶) ∈ P)
44 mulclpr 7562 . . . . . 6 ((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) → (𝐴 ·P (𝐵 +P 𝐶)) ∈ P)
4540, 43, 44syl2anc 411 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝐴 ·P (𝐵 +P 𝐶)) ∈ P)
46 distrnqg 7377 . . . . . . 7 ((𝑓Q𝑦Q𝑧Q) → (𝑓 ·Q (𝑦 +Q 𝑧)) = ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
4712, 18, 33, 46syl3anc 1238 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q (𝑦 +Q 𝑧)) = ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
48 simprrl 539 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑓 ∈ (1st𝐴))
49 df-iplp 7458 . . . . . . . . . 10 +P = (𝑢P, 𝑣P ↦ ⟨{𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑢) ∧ ∈ (1st𝑣) ∧ 𝑤 = (𝑔 +Q ))}, {𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑢) ∧ ∈ (2nd𝑣) ∧ 𝑤 = (𝑔 +Q ))}⟩)
50 addclnq 7365 . . . . . . . . . 10 ((𝑔QQ) → (𝑔 +Q ) ∈ Q)
5149, 50genpprecll 7504 . . . . . . . . 9 ((𝐵P𝐶P) → ((𝑦 ∈ (1st𝐵) ∧ 𝑧 ∈ (1st𝐶)) → (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶))))
5251imp 124 . . . . . . . 8 (((𝐵P𝐶P) ∧ (𝑦 ∈ (1st𝐵) ∧ 𝑧 ∈ (1st𝐶))) → (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))
5313, 28, 14, 29, 52syl22anc 1239 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))
54 df-imp 7459 . . . . . . . . 9 ·P = (𝑢P, 𝑣P ↦ ⟨{𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑢) ∧ ∈ (1st𝑣) ∧ 𝑤 = (𝑔 ·Q ))}, {𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑢) ∧ ∈ (2nd𝑣) ∧ 𝑤 = (𝑔 ·Q ))}⟩)
55 mulclnq 7366 . . . . . . . . 9 ((𝑔QQ) → (𝑔 ·Q ) ∈ Q)
5654, 55genpprecll 7504 . . . . . . . 8 ((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) → ((𝑓 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶))) → (𝑓 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
5756imp 124 . . . . . . 7 (((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) ∧ (𝑓 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))) → (𝑓 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
5840, 43, 48, 53, 57syl22anc 1239 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
5947, 58eqeltrrd 2255 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
60 prop 7465 . . . . . 6 ((𝐴 ·P (𝐵 +P 𝐶)) ∈ P → ⟨(1st ‘(𝐴 ·P (𝐵 +P 𝐶))), (2nd ‘(𝐴 ·P (𝐵 +P 𝐶)))⟩ ∈ P)
61 prcdnql 7474 . . . . . 6 ((⟨(1st ‘(𝐴 ·P (𝐵 +P 𝐶))), (2nd ‘(𝐴 ·P (𝐵 +P 𝐶)))⟩ ∈ P ∧ ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
6260, 61sylan 283 . . . . 5 (((𝐴 ·P (𝐵 +P 𝐶)) ∈ P ∧ ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
6345, 59, 62syl2anc 411 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
6439, 63sylbid 150 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 <Q 𝑓 → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
652, 12, 8, 33, 20caovord2d 6038 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 <Q 𝑥 ↔ (𝑓 ·Q 𝑧) <Q (𝑥 ·Q 𝑧)))
66 mulclnq 7366 . . . . . . 7 ((𝑥Q𝑧Q) → (𝑥 ·Q 𝑧) ∈ Q)
678, 33, 66syl2anc 411 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q 𝑧) ∈ Q)
68 ltanqg 7390 . . . . . 6 (((𝑓 ·Q 𝑧) ∈ Q ∧ (𝑥 ·Q 𝑧) ∈ Q ∧ (𝑥 ·Q 𝑦) ∈ Q) → ((𝑓 ·Q 𝑧) <Q (𝑥 ·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧))))
6935, 67, 25, 68syl3anc 1238 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑓 ·Q 𝑧) <Q (𝑥 ·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧))))
7065, 69bitrd 188 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 <Q 𝑥 ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧))))
71 distrnqg 7377 . . . . . . 7 ((𝑥Q𝑦Q𝑧Q) → (𝑥 ·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)))
728, 18, 33, 71syl3anc 1238 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)))
73 simprll 537 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑥 ∈ (1st𝐴))
7454, 55genpprecll 7504 . . . . . . . 8 ((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) → ((𝑥 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶))) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
7574imp 124 . . . . . . 7 (((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) ∧ (𝑥 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
7640, 43, 73, 53, 75syl22anc 1239 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
7772, 76eqeltrrd 2255 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
78 prcdnql 7474 . . . . . 6 ((⟨(1st ‘(𝐴 ·P (𝐵 +P 𝐶))), (2nd ‘(𝐴 ·P (𝐵 +P 𝐶)))⟩ ∈ P ∧ ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
7960, 78sylan 283 . . . . 5 (((𝐴 ·P (𝐵 +P 𝐶)) ∈ P ∧ ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
8045, 77, 79syl2anc 411 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
8170, 80sylbid 150 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 <Q 𝑥 → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
8264, 81jaod 717 . 2 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 <Q 𝑓𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
83 ltsonq 7388 . . . . 5 <Q Or Q
84 nqtri3or 7386 . . . . 5 ((𝑥Q𝑓Q) → (𝑥 <Q 𝑓𝑥 = 𝑓𝑓 <Q 𝑥))
8583, 84sotritrieq 4322 . . . 4 ((𝑥Q𝑓Q) → (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
868, 12, 85syl2anc 411 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
87 oveq1 5876 . . . . . . 7 (𝑥 = 𝑓 → (𝑥 ·Q 𝑧) = (𝑓 ·Q 𝑧))
8887oveq2d 5885 . . . . . 6 (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
8972, 88sylan9eq 2230 . . . . 5 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ 𝑥 = 𝑓) → (𝑥 ·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
9076adantr 276 . . . . 5 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ 𝑥 = 𝑓) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
9189, 90eqeltrrd 2255 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ 𝑥 = 𝑓) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
9291ex 115 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
9386, 92sylbird 170 . 2 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
94 ltdcnq 7387 . . . . 5 ((𝑥Q𝑓Q) → DECID 𝑥 <Q 𝑓)
95 ltdcnq 7387 . . . . . 6 ((𝑓Q𝑥Q) → DECID 𝑓 <Q 𝑥)
9695ancoms 268 . . . . 5 ((𝑥Q𝑓Q) → DECID 𝑓 <Q 𝑥)
97 dcor 935 . . . . 5 (DECID 𝑥 <Q 𝑓 → (DECID 𝑓 <Q 𝑥DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
9894, 96, 97sylc 62 . . . 4 ((𝑥Q𝑓Q) → DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥))
998, 12, 98syl2anc 411 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥))
100 df-dc 835 . . 3 (DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥) ↔ ((𝑥 <Q 𝑓𝑓 <Q 𝑥) ∨ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
10199, 100sylib 122 . 2 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 <Q 𝑓𝑓 <Q 𝑥) ∨ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
10282, 93, 101mpjaod 718 1 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834  w3a 978   = wceq 1353  wcel 2148  cop 3594   class class class wbr 4000  cfv 5212  (class class class)co 5869  1st c1st 6133  2nd c2nd 6134  Qcnq 7270   +Q cplq 7272   ·Q cmq 7273   <Q cltq 7275  Pcnp 7281   +P cpp 7283   ·P cmp 7284
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 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584
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 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-eprel 4286  df-id 4290  df-po 4293  df-iso 4294  df-iord 4363  df-on 4365  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-irdg 6365  df-1o 6411  df-2o 6412  df-oadd 6415  df-omul 6416  df-er 6529  df-ec 6531  df-qs 6535  df-ni 7294  df-pli 7295  df-mi 7296  df-lti 7297  df-plpq 7334  df-mpq 7335  df-enq 7337  df-nqqs 7338  df-plqqs 7339  df-mqqs 7340  df-1nqqs 7341  df-rq 7342  df-ltnqqs 7343  df-enq0 7414  df-nq0 7415  df-0nq0 7416  df-plq0 7417  df-mq0 7418  df-inp 7456  df-iplp 7458  df-imp 7459
This theorem is referenced by:  distrlem5prl  7576
  Copyright terms: Public domain W3C validator