Metamath Proof Explorer

Theorem distrlem1pr

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

Ref Expression
Assertion distrlem1pr ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ⊆ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 addclpr ⊢ ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 +P 𝐶 ) ∈ P )
2 df-mp ⊢ ·P = ( 𝑦 ∈ P , 𝑧 ∈ P ↦ { 𝑓 ∣ ∃ 𝑔 ∈ 𝑦 ∃ ℎ ∈ 𝑧 𝑓 = ( 𝑔 ·Q ℎ ) } )
3 mulclnq ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 ·Q ℎ ) ∈ Q )
4 2 3 genpelv ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 +P 𝐶 ) ∈ P ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐵 +P 𝐶 ) 𝑤 = ( 𝑥 ·Q 𝑣 ) ) )
5 1 4 sylan2 ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐵 +P 𝐶 ) 𝑤 = ( 𝑥 ·Q 𝑣 ) ) )
6 5 3impb ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐵 +P 𝐶 ) 𝑤 = ( 𝑥 ·Q 𝑣 ) ) )
7 df-plp ⊢ +P = ( 𝑤 ∈ P , 𝑥 ∈ P ↦ { 𝑓 ∣ ∃ 𝑔 ∈ 𝑤 ∃ ℎ ∈ 𝑥 𝑓 = ( 𝑔 +Q ℎ ) } )
8 addclnq ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 +Q ℎ ) ∈ Q )
9 7 8 genpelv ⊢ ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑣 ∈ ( 𝐵 +P 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑣 = ( 𝑦 +Q 𝑧 ) ) )
10 9 3adant1 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑣 ∈ ( 𝐵 +P 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑣 = ( 𝑦 +Q 𝑧 ) ) )
11 10 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) → ( 𝑣 ∈ ( 𝐵 +P 𝐶 ) ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑣 = ( 𝑦 +Q 𝑧 ) ) )
12 simprr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) → 𝑤 = ( 𝑥 ·Q 𝑣 ) )
13 simpr ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) → 𝑣 = ( 𝑦 +Q 𝑧 ) )
14 oveq2 ⊢ ( 𝑣 = ( 𝑦 +Q 𝑧 ) → ( 𝑥 ·Q 𝑣 ) = ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) )
15 14 eqeq2d ⊢ ( 𝑣 = ( 𝑦 +Q 𝑧 ) → ( 𝑤 = ( 𝑥 ·Q 𝑣 ) ↔ 𝑤 = ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) ) )
16 15 biimpac ⊢ ( ( 𝑤 = ( 𝑥 ·Q 𝑣 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) → 𝑤 = ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) )
17 distrnq ⊢ ( 𝑥 ·Q ( 𝑦 +Q 𝑧 ) ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) )
18 16 17 eqtrdi ⊢ ( ( 𝑤 = ( 𝑥 ·Q 𝑣 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) → 𝑤 = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) )
19 12 13 18 syl2an ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → 𝑤 = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) )
20 mulclpr ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ·P 𝐵 ) ∈ P )
21 20 3adant3 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P 𝐵 ) ∈ P )
22 21 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → ( 𝐴 ·P 𝐵 ) ∈ P )
23 mulclpr ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P 𝐶 ) ∈ P )
24 23 3adant2 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P 𝐶 ) ∈ P )
25 24 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → ( 𝐴 ·P 𝐶 ) ∈ P )
26 simpll ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) → 𝑦 ∈ 𝐵 )
27 2 3 genpprecl ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) ) )
28 27 3adant3 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) ) )
29 28 impl ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) )
30 29 adantlrr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) )
31 26 30 sylan2 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) )
32 simplr ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) → 𝑧 ∈ 𝐶 )
33 2 3 genpprecl ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) ) )
34 33 3adant2 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) ) )
35 34 impl ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) )
36 35 adantlrr ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) )
37 32 36 sylan2 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) )
38 7 8 genpprecl ⊢ ( ( ( 𝐴 ·P 𝐵 ) ∈ P ∧ ( 𝐴 ·P 𝐶 ) ∈ P ) → ( ( ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) ∧ ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) )
39 38 imp ⊢ ( ( ( ( 𝐴 ·P 𝐵 ) ∈ P ∧ ( 𝐴 ·P 𝐶 ) ∈ P ) ∧ ( ( 𝑥 ·Q 𝑦 ) ∈ ( 𝐴 ·P 𝐵 ) ∧ ( 𝑥 ·Q 𝑧 ) ∈ ( 𝐴 ·P 𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )
40 22 25 31 37 39 syl22anc ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑥 ·Q 𝑧 ) ) ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )
41 19 40 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑣 = ( 𝑦 +Q 𝑧 ) ) ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )
42 41 exp32 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑣 = ( 𝑦 +Q 𝑧 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) ) )
43 42 rexlimdvv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑣 = ( 𝑦 +Q 𝑧 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) )
44 11 43 sylbid ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑤 = ( 𝑥 ·Q 𝑣 ) ) ) → ( 𝑣 ∈ ( 𝐵 +P 𝐶 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) )
45 44 exp32 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑥 ∈ 𝐴 → ( 𝑤 = ( 𝑥 ·Q 𝑣 ) → ( 𝑣 ∈ ( 𝐵 +P 𝐶 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) ) ) )
46 45 com34 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑥 ∈ 𝐴 → ( 𝑣 ∈ ( 𝐵 +P 𝐶 ) → ( 𝑤 = ( 𝑥 ·Q 𝑣 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) ) ) )
47 46 impd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑣 ∈ ( 𝐵 +P 𝐶 ) ) → ( 𝑤 = ( 𝑥 ·Q 𝑣 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) ) )
48 47 rexlimdvv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑣 ∈ ( 𝐵 +P 𝐶 ) 𝑤 = ( 𝑥 ·Q 𝑣 ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) )
49 6 48 sylbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) → 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ) )
50 49 ssrdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ⊆ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) )