Metamath Proof Explorer


Theorem distrlem4pr

Description: Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion distrlem4pr ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 simpl2 ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝐵P )
2 simprlr ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑦𝐵 )
3 elprnq ( ( 𝐵P𝑦𝐵 ) → 𝑦Q )
4 1 2 3 syl2anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑦Q )
5 simp1 ( ( 𝐴P𝐵P𝐶P ) → 𝐴P )
6 simprl ( ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) → 𝑓𝐴 )
7 elprnq ( ( 𝐴P𝑓𝐴 ) → 𝑓Q )
8 5 6 7 syl2an ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑓Q )
9 simpl3 ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝐶P )
10 simprrr ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑧𝐶 )
11 elprnq ( ( 𝐶P𝑧𝐶 ) → 𝑧Q )
12 9 10 11 syl2anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑧Q )
13 vex 𝑥 ∈ V
14 vex 𝑓 ∈ V
15 ltmnq ( 𝑢Q → ( 𝑤 <Q 𝑣 ↔ ( 𝑢 ·Q 𝑤 ) <Q ( 𝑢 ·Q 𝑣 ) ) )
16 vex 𝑦 ∈ V
17 mulcomnq ( 𝑤 ·Q 𝑣 ) = ( 𝑣 ·Q 𝑤 )
18 13 14 15 16 17 caovord2 ( 𝑦Q → ( 𝑥 <Q 𝑓 ↔ ( 𝑥 ·Q 𝑦 ) <Q ( 𝑓 ·Q 𝑦 ) ) )
19 mulclnq ( ( 𝑓Q𝑧Q ) → ( 𝑓 ·Q 𝑧 ) ∈ Q )
20 ovex ( 𝑥 ·Q 𝑦 ) ∈ V
21 ovex ( 𝑓 ·Q 𝑦 ) ∈ V
22 ltanq ( 𝑢Q → ( 𝑤 <Q 𝑣 ↔ ( 𝑢 +Q 𝑤 ) <Q ( 𝑢 +Q 𝑣 ) ) )
23 ovex ( 𝑓 ·Q 𝑧 ) ∈ V
24 addcomnq ( 𝑤 +Q 𝑣 ) = ( 𝑣 +Q 𝑤 )
25 20 21 22 23 24 caovord2 ( ( 𝑓 ·Q 𝑧 ) ∈ Q → ( ( 𝑥 ·Q 𝑦 ) <Q ( 𝑓 ·Q 𝑦 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) )
26 19 25 syl ( ( 𝑓Q𝑧Q ) → ( ( 𝑥 ·Q 𝑦 ) <Q ( 𝑓 ·Q 𝑦 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) )
27 18 26 sylan9bb ( ( 𝑦Q ∧ ( 𝑓Q𝑧Q ) ) → ( 𝑥 <Q 𝑓 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) )
28 4 8 12 27 syl12anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑥 <Q 𝑓 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) )
29 simpl1 ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝐴P )
30 addclpr ( ( 𝐵P𝐶P ) → ( 𝐵 +P 𝐶 ) ∈ P )
31 30 3adant1 ( ( 𝐴P𝐵P𝐶P ) → ( 𝐵 +P 𝐶 ) ∈ P )
32 31 adantr ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝐵 +P 𝐶 ) ∈ P )
33 mulclpr ( ( 𝐴P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ∈ P )
34 29 32 33 syl2anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ∈ P )
35 distrnq ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) )
36 simprrl ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑓𝐴 )
37 df-plp +P = ( 𝑢P , 𝑣P ↦ { 𝑤 ∣ ∃ 𝑔𝑢𝑣 𝑤 = ( 𝑔 +Q ) } )
38 addclnq ( ( 𝑔QQ ) → ( 𝑔 +Q ) ∈ Q )
39 37 38 genpprecl ( ( 𝐵P𝐶P ) → ( ( 𝑦𝐵𝑧𝐶 ) → ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) )
40 39 imp ( ( ( 𝐵P𝐶P ) ∧ ( 𝑦𝐵𝑧𝐶 ) ) → ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) )
41 1 9 2 10 40 syl22anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) )
42 df-mp ·P = ( 𝑢P , 𝑣P ↦ { 𝑤 ∣ ∃ 𝑔𝑢𝑣 𝑤 = ( 𝑔 ·Q ) } )
43 mulclnq ( ( 𝑔QQ ) → ( 𝑔 ·Q ) ∈ Q )
44 42 43 genpprecl ( ( 𝐴P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( ( 𝑓𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) → ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
45 44 imp ( ( ( 𝐴P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) ∧ ( 𝑓𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) ) → ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
46 29 32 36 41 45 syl22anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑓 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
47 35 46 eqeltrrid ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
48 prcdnq ( ( ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ∈ P ∧ ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) → ( ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
49 34 47 48 syl2anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑓 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
50 28 49 sylbid ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑥 <Q 𝑓 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
51 simpll ( ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) → 𝑥𝐴 )
52 elprnq ( ( 𝐴P𝑥𝐴 ) → 𝑥Q )
53 5 51 52 syl2an ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑥Q )
54 vex 𝑧 ∈ V
55 14 13 15 54 17 caovord2 ( 𝑧Q → ( 𝑓 <Q 𝑥 ↔ ( 𝑓 ·Q 𝑧 ) <Q ( 𝑥 ·Q 𝑧 ) ) )
56 mulclnq ( ( 𝑥Q𝑦Q ) → ( 𝑥 ·Q 𝑦 ) ∈ Q )
57 ltanq ( ( 𝑥 ·Q 𝑦 ) ∈ Q → ( ( 𝑓 ·Q 𝑧 ) <Q ( 𝑥 ·Q 𝑧 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) )
58 56 57 syl ( ( 𝑥Q𝑦Q ) → ( ( 𝑓 ·Q 𝑧 ) <Q ( 𝑥 ·Q 𝑧 ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) )
59 55 58 sylan9bbr ( ( ( 𝑥Q𝑦Q ) ∧ 𝑧Q ) → ( 𝑓 <Q 𝑥 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) )
60 53 4 12 59 syl21anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑓 <Q 𝑥 ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ) )
61 distrnq ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) )
62 simprll ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → 𝑥𝐴 )
63 42 43 genpprecl ( ( 𝐴P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( ( 𝑥𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
64 63 imp ( ( ( 𝐴P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) ∧ ( 𝑥𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ ( 𝐵 +P 𝐶 ) ) ) → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
65 29 32 62 41 64 syl22anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
66 61 65 eqeltrrid ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
67 prcdnq ( ( ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ∈ P ∧ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) → ( ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
68 34 66 67 syl2anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) <Q ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
69 60 68 sylbid ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑓 <Q 𝑥 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
70 ltsonq <Q Or Q
71 sotrieq ( ( <Q Or Q ∧ ( 𝑥Q𝑓Q ) ) → ( 𝑥 = 𝑓 ↔ ¬ ( 𝑥 <Q 𝑓𝑓 <Q 𝑥 ) ) )
72 70 71 mpan ( ( 𝑥Q𝑓Q ) → ( 𝑥 = 𝑓 ↔ ¬ ( 𝑥 <Q 𝑓𝑓 <Q 𝑥 ) ) )
73 53 8 72 syl2anc ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑥 = 𝑓 ↔ ¬ ( 𝑥 <Q 𝑓𝑓 <Q 𝑥 ) ) )
74 oveq1 ( 𝑥 = 𝑓 → ( 𝑥 ·Q 𝑧 ) = ( 𝑓 ·Q 𝑧 ) )
75 74 oveq2d ( 𝑥 = 𝑓 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) )
76 61 75 eqtrid ( 𝑥 = 𝑓 → ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) )
77 76 eleq1d ( 𝑥 = 𝑓 → ( ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
78 65 77 syl5ibcom ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( 𝑥 = 𝑓 → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
79 73 78 sylbird ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ¬ ( 𝑥 <Q 𝑓𝑓 <Q 𝑥 ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
80 50 69 79 ecase3d ( ( ( 𝐴P𝐵P𝐶P ) ∧ ( ( 𝑥𝐴𝑦𝐵 ) ∧ ( 𝑓𝐴𝑧𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )