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

Theorem distrlem4prl 6825
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 6642 . . . . . . 7 ((𝑤Q𝑣Q𝑢Q) → (𝑤 <Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q (𝑢 ·Q 𝑣)))
21adantl 271 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q𝑢Q)) → (𝑤 <Q 𝑣 ↔ (𝑢 ·Q 𝑤) <Q (𝑢 ·Q 𝑣)))
3 simp1 939 . . . . . . 7 ((𝐴P𝐵P𝐶P) → 𝐴P)
4 simpll 496 . . . . . . 7 (((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶))) → 𝑥 ∈ (1st𝐴))
5 prop 6716 . . . . . . . 8 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
6 elprnql 6722 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑥 ∈ (1st𝐴)) → 𝑥Q)
75, 6sylan 277 . . . . . . 7 ((𝐴P𝑥 ∈ (1st𝐴)) → 𝑥Q)
83, 4, 7syl2an 283 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑥Q)
9 simprl 498 . . . . . . 7 (((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶))) → 𝑓 ∈ (1st𝐴))
10 elprnql 6722 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑓 ∈ (1st𝐴)) → 𝑓Q)
115, 10sylan 277 . . . . . . 7 ((𝐴P𝑓 ∈ (1st𝐴)) → 𝑓Q)
123, 9, 11syl2an 283 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑓Q)
13 simpl2 943 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝐵P)
14 simprlr 505 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑦 ∈ (1st𝐵))
15 prop 6716 . . . . . . . 8 (𝐵P → ⟨(1st𝐵), (2nd𝐵)⟩ ∈ P)
16 elprnql 6722 . . . . . . . 8 ((⟨(1st𝐵), (2nd𝐵)⟩ ∈ P𝑦 ∈ (1st𝐵)) → 𝑦Q)
1715, 16sylan 277 . . . . . . 7 ((𝐵P𝑦 ∈ (1st𝐵)) → 𝑦Q)
1813, 14, 17syl2anc 403 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑦Q)
19 mulcomnqg 6624 . . . . . . 7 ((𝑤Q𝑣Q) → (𝑤 ·Q 𝑣) = (𝑣 ·Q 𝑤))
2019adantl 271 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q)) → (𝑤 ·Q 𝑣) = (𝑣 ·Q 𝑤))
212, 8, 12, 18, 20caovord2d 5695 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 <Q 𝑓 ↔ (𝑥 ·Q 𝑦) <Q (𝑓 ·Q 𝑦)))
22 ltanqg 6641 . . . . . . 7 ((𝑤Q𝑣Q𝑢Q) → (𝑤 <Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q (𝑢 +Q 𝑣)))
2322adantl 271 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q𝑢Q)) → (𝑤 <Q 𝑣 ↔ (𝑢 +Q 𝑤) <Q (𝑢 +Q 𝑣)))
24 mulclnq 6617 . . . . . . 7 ((𝑥Q𝑦Q) → (𝑥 ·Q 𝑦) ∈ Q)
258, 18, 24syl2anc 403 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q 𝑦) ∈ Q)
26 mulclnq 6617 . . . . . . 7 ((𝑓Q𝑦Q) → (𝑓 ·Q 𝑦) ∈ Q)
2712, 18, 26syl2anc 403 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q 𝑦) ∈ Q)
28 simpl3 944 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝐶P)
29 simprrr 507 . . . . . . . 8 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑧 ∈ (1st𝐶))
30 prop 6716 . . . . . . . . 9 (𝐶P → ⟨(1st𝐶), (2nd𝐶)⟩ ∈ P)
31 elprnql 6722 . . . . . . . . 9 ((⟨(1st𝐶), (2nd𝐶)⟩ ∈ P𝑧 ∈ (1st𝐶)) → 𝑧Q)
3230, 31sylan 277 . . . . . . . 8 ((𝐶P𝑧 ∈ (1st𝐶)) → 𝑧Q)
3328, 29, 32syl2anc 403 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑧Q)
34 mulclnq 6617 . . . . . . 7 ((𝑓Q𝑧Q) → (𝑓 ·Q 𝑧) ∈ Q)
3512, 33, 34syl2anc 403 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q 𝑧) ∈ Q)
36 addcomnqg 6622 . . . . . . 7 ((𝑤Q𝑣Q) → (𝑤 +Q 𝑣) = (𝑣 +Q 𝑤))
3736adantl 271 . . . . . 6 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ (𝑤Q𝑣Q)) → (𝑤 +Q 𝑣) = (𝑣 +Q 𝑤))
3823, 25, 27, 35, 37caovord2d 5695 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 ·Q 𝑦) <Q (𝑓 ·Q 𝑦) ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧))))
3921, 38bitrd 186 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 <Q 𝑓 ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧))))
40 simpl1 942 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝐴P)
41 addclpr 6778 . . . . . . . 8 ((𝐵P𝐶P) → (𝐵 +P 𝐶) ∈ P)
42413adant1 957 . . . . . . 7 ((𝐴P𝐵P𝐶P) → (𝐵 +P 𝐶) ∈ P)
4342adantr 270 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝐵 +P 𝐶) ∈ P)
44 mulclpr 6813 . . . . . 6 ((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) → (𝐴 ·P (𝐵 +P 𝐶)) ∈ P)
4540, 43, 44syl2anc 403 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝐴 ·P (𝐵 +P 𝐶)) ∈ P)
46 distrnqg 6628 . . . . . . 7 ((𝑓Q𝑦Q𝑧Q) → (𝑓 ·Q (𝑦 +Q 𝑧)) = ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
4712, 18, 33, 46syl3anc 1170 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q (𝑦 +Q 𝑧)) = ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
48 simprrl 506 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑓 ∈ (1st𝐴))
49 df-iplp 6709 . . . . . . . . . 10 +P = (𝑢P, 𝑣P ↦ ⟨{𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑢) ∧ ∈ (1st𝑣) ∧ 𝑤 = (𝑔 +Q ))}, {𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑢) ∧ ∈ (2nd𝑣) ∧ 𝑤 = (𝑔 +Q ))}⟩)
50 addclnq 6616 . . . . . . . . . 10 ((𝑔QQ) → (𝑔 +Q ) ∈ Q)
5149, 50genpprecll 6755 . . . . . . . . 9 ((𝐵P𝐶P) → ((𝑦 ∈ (1st𝐵) ∧ 𝑧 ∈ (1st𝐶)) → (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶))))
5251imp 122 . . . . . . . 8 (((𝐵P𝐶P) ∧ (𝑦 ∈ (1st𝐵) ∧ 𝑧 ∈ (1st𝐶))) → (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))
5313, 28, 14, 29, 52syl22anc 1171 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))
54 df-imp 6710 . . . . . . . . 9 ·P = (𝑢P, 𝑣P ↦ ⟨{𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (1st𝑢) ∧ ∈ (1st𝑣) ∧ 𝑤 = (𝑔 ·Q ))}, {𝑤Q ∣ ∃𝑔QQ (𝑔 ∈ (2nd𝑢) ∧ ∈ (2nd𝑣) ∧ 𝑤 = (𝑔 ·Q ))}⟩)
55 mulclnq 6617 . . . . . . . . 9 ((𝑔QQ) → (𝑔 ·Q ) ∈ Q)
5654, 55genpprecll 6755 . . . . . . . 8 ((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) → ((𝑓 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶))) → (𝑓 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
5756imp 122 . . . . . . 7 (((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) ∧ (𝑓 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))) → (𝑓 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
5840, 43, 48, 53, 57syl22anc 1171 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
5947, 58eqeltrrd 2157 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
60 prop 6716 . . . . . 6 ((𝐴 ·P (𝐵 +P 𝐶)) ∈ P → ⟨(1st ‘(𝐴 ·P (𝐵 +P 𝐶))), (2nd ‘(𝐴 ·P (𝐵 +P 𝐶)))⟩ ∈ P)
61 prcdnql 6725 . . . . . 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 277 . . . . 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 403 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑓 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
6439, 63sylbid 148 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 <Q 𝑓 → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
652, 12, 8, 33, 20caovord2d 5695 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 <Q 𝑥 ↔ (𝑓 ·Q 𝑧) <Q (𝑥 ·Q 𝑧)))
66 mulclnq 6617 . . . . . . 7 ((𝑥Q𝑧Q) → (𝑥 ·Q 𝑧) ∈ Q)
678, 33, 66syl2anc 403 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q 𝑧) ∈ Q)
68 ltanqg 6641 . . . . . 6 (((𝑓 ·Q 𝑧) ∈ Q ∧ (𝑥 ·Q 𝑧) ∈ Q ∧ (𝑥 ·Q 𝑦) ∈ Q) → ((𝑓 ·Q 𝑧) <Q (𝑥 ·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧))))
6935, 67, 25, 68syl3anc 1170 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑓 ·Q 𝑧) <Q (𝑥 ·Q 𝑧) ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧))))
7065, 69bitrd 186 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 <Q 𝑥 ↔ ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧))))
71 distrnqg 6628 . . . . . . 7 ((𝑥Q𝑦Q𝑧Q) → (𝑥 ·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)))
728, 18, 33, 71syl3anc 1170 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)))
73 simprll 504 . . . . . . 7 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → 𝑥 ∈ (1st𝐴))
7454, 55genpprecll 6755 . . . . . . . 8 ((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) → ((𝑥 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶))) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
7574imp 122 . . . . . . 7 (((𝐴P ∧ (𝐵 +P 𝐶) ∈ P) ∧ (𝑥 ∈ (1st𝐴) ∧ (𝑦 +Q 𝑧) ∈ (1st ‘(𝐵 +P 𝐶)))) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
7640, 43, 73, 53, 75syl22anc 1171 . . . . . 6 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
7772, 76eqeltrrd 2157 . . . . 5 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
78 prcdnql 6725 . . . . . 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 277 . . . . 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 403 . . . 4 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) <Q ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
8170, 80sylbid 148 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑓 <Q 𝑥 → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
8264, 81jaod 670 . 2 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 <Q 𝑓𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
83 ltsonq 6639 . . . . 5 <Q Or Q
84 nqtri3or 6637 . . . . 5 ((𝑥Q𝑓Q) → (𝑥 <Q 𝑓𝑥 = 𝑓𝑓 <Q 𝑥))
8583, 84sotritrieq 4082 . . . 4 ((𝑥Q𝑓Q) → (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
868, 12, 85syl2anc 403 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 = 𝑓 ↔ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
87 oveq1 5544 . . . . . . 7 (𝑥 = 𝑓 → (𝑥 ·Q 𝑧) = (𝑓 ·Q 𝑧))
8887oveq2d 5553 . . . . . 6 (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q (𝑥 ·Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
8972, 88sylan9eq 2134 . . . . 5 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ 𝑥 = 𝑓) → (𝑥 ·Q (𝑦 +Q 𝑧)) = ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)))
9076adantr 270 . . . . 5 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ 𝑥 = 𝑓) → (𝑥 ·Q (𝑦 +Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
9189, 90eqeltrrd 2157 . . . 4 ((((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) ∧ 𝑥 = 𝑓) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶))))
9291ex 113 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (𝑥 = 𝑓 → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
9386, 92sylbird 168 . 2 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → (¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥) → ((𝑥 ·Q 𝑦) +Q (𝑓 ·Q 𝑧)) ∈ (1st ‘(𝐴 ·P (𝐵 +P 𝐶)))))
94 ltdcnq 6638 . . . . 5 ((𝑥Q𝑓Q) → DECID 𝑥 <Q 𝑓)
95 ltdcnq 6638 . . . . . 6 ((𝑓Q𝑥Q) → DECID 𝑓 <Q 𝑥)
9695ancoms 264 . . . . 5 ((𝑥Q𝑓Q) → DECID 𝑓 <Q 𝑥)
97 dcor 877 . . . . 5 (DECID 𝑥 <Q 𝑓 → (DECID 𝑓 <Q 𝑥DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
9894, 96, 97sylc 61 . . . 4 ((𝑥Q𝑓Q) → DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥))
998, 12, 98syl2anc 403 . . 3 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥))
100 df-dc 777 . . 3 (DECID (𝑥 <Q 𝑓𝑓 <Q 𝑥) ↔ ((𝑥 <Q 𝑓𝑓 <Q 𝑥) ∨ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
10199, 100sylib 120 . 2 (((𝐴P𝐵P𝐶P) ∧ ((𝑥 ∈ (1st𝐴) ∧ 𝑦 ∈ (1st𝐵)) ∧ (𝑓 ∈ (1st𝐴) ∧ 𝑧 ∈ (1st𝐶)))) → ((𝑥 <Q 𝑓𝑓 <Q 𝑥) ∨ ¬ (𝑥 <Q 𝑓𝑓 <Q 𝑥)))
10282, 93, 101mpjaod 671 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 102  wb 103  wo 662  DECID wdc 776  w3a 920   = wceq 1285  wcel 1434  cop 3403   class class class wbr 3787  cfv 4926  (class class class)co 5537  1st c1st 5790  2nd c2nd 5791  Qcnq 6521   +Q cplq 6523   ·Q cmq 6524   <Q cltq 6526  Pcnp 6532   +P cpp 6534   ·P cmp 6535
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 2064  ax-coll 3895  ax-sep 3898  ax-nul 3906  ax-pow 3950  ax-pr 3966  ax-un 4190  ax-setind 4282  ax-iinf 4331
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 1687  df-eu 1945  df-mo 1946  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-ne 2247  df-ral 2354  df-rex 2355  df-reu 2356  df-rab 2358  df-v 2604  df-sbc 2817  df-csb 2910  df-dif 2976  df-un 2978  df-in 2980  df-ss 2987  df-nul 3253  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3604  df-int 3639  df-iun 3682  df-br 3788  df-opab 3842  df-mpt 3843  df-tr 3878  df-eprel 4046  df-id 4050  df-po 4053  df-iso 4054  df-iord 4123  df-on 4125  df-suc 4128  df-iom 4334  df-xp 4371  df-rel 4372  df-cnv 4373  df-co 4374  df-dm 4375  df-rn 4376  df-res 4377  df-ima 4378  df-iota 4891  df-fun 4928  df-fn 4929  df-f 4930  df-f1 4931  df-fo 4932  df-f1o 4933  df-fv 4934  df-ov 5540  df-oprab 5541  df-mpt2 5542  df-1st 5792  df-2nd 5793  df-recs 5948  df-irdg 6013  df-1o 6059  df-2o 6060  df-oadd 6063  df-omul 6064  df-er 6165  df-ec 6167  df-qs 6171  df-ni 6545  df-pli 6546  df-mi 6547  df-lti 6548  df-plpq 6585  df-mpq 6586  df-enq 6588  df-nqqs 6589  df-plqqs 6590  df-mqqs 6591  df-1nqqs 6592  df-rq 6593  df-ltnqqs 6594  df-enq0 6665  df-nq0 6666  df-0nq0 6667  df-plq0 6668  df-mq0 6669  df-inp 6707  df-iplp 6709  df-imp 6710
This theorem is referenced by:  distrlem5prl  6827
  Copyright terms: Public domain W3C validator