Metamath Proof Explorer

Theorem distrlem5pr

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 distrlem5pr ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ⊆ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 mulclpr ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ·P 𝐵 ) ∈ P )
2 1 3adant3 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P 𝐵 ) ∈ P )
3 mulclpr ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 ·P 𝐶 ) ∈ P )
4 df-plp ⊢ +P = ( 𝑥 ∈ P , 𝑦 ∈ P ↦ { 𝑓 ∣ ∃ 𝑔 ∈ 𝑥 ∃ ℎ ∈ 𝑦 𝑓 = ( 𝑔 +Q ℎ ) } )
5 addclnq ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 +Q ℎ ) ∈ Q )
6 4 5 genpelv ⊢ ( ( ( 𝐴 ·P 𝐵 ) ∈ P ∧ ( 𝐴 ·P 𝐶 ) ∈ P ) → ( 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ↔ ∃ 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∃ 𝑢 ∈ ( 𝐴 ·P 𝐶 ) 𝑤 = ( 𝑣 +Q 𝑢 ) ) )
7 2 3 6 3imp3i2an ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ↔ ∃ 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∃ 𝑢 ∈ ( 𝐴 ·P 𝐶 ) 𝑤 = ( 𝑣 +Q 𝑢 ) ) )
8 df-mp ⊢ ·P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑔 ∈ 𝑤 ∃ ℎ ∈ 𝑣 𝑥 = ( 𝑔 ·Q ℎ ) } )
9 mulclnq ⊢ ( ( 𝑔 ∈ Q ∧ ℎ ∈ Q ) → ( 𝑔 ·Q ℎ ) ∈ Q )
10 8 9 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑢 ∈ ( 𝐴 ·P 𝐶 ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) ) )
11 10 3adant2 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑢 ∈ ( 𝐴 ·P 𝐶 ) ↔ ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) ) )
12 11 anbi2d ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 ·P 𝐶 ) ) ↔ ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∧ ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) ) ) )
13 df-mp ⊢ ·P = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑓 ∣ ∃ 𝑔 ∈ 𝑤 ∃ ℎ ∈ 𝑣 𝑓 = ( 𝑔 ·Q ℎ ) } )
14 13 9 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑣 = ( 𝑥 ·Q 𝑦 ) ) )
15 14 3adant3 ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑣 = ( 𝑥 ·Q 𝑦 ) ) )
16 distrlem4pr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )
17 oveq12 ⊢ ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) → ( 𝑣 +Q 𝑢 ) = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) )
18 17 eqeq2d ⊢ ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) ↔ 𝑤 = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ) )
19 eleq1 ⊢ ( 𝑤 = ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
20 18 19 syl6bi ⊢ ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) )
21 20 imp ⊢ ( ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) ∧ 𝑤 = ( 𝑣 +Q 𝑢 ) ) → ( 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ↔ ( ( 𝑥 ·Q 𝑦 ) +Q ( 𝑓 ·Q 𝑧 ) ) ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
22 16 21 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) ) → ( ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) ∧ 𝑤 = ( 𝑣 +Q 𝑢 ) ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
23 22 exp4b ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) )
24 23 com3l ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝑣 = ( 𝑥 ·Q 𝑦 ) ∧ 𝑢 = ( 𝑓 ·Q 𝑧 ) ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) )
25 24 exp4b ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑣 = ( 𝑥 ·Q 𝑦 ) → ( 𝑢 = ( 𝑓 ·Q 𝑧 ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) ) ) )
26 25 com23 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑣 = ( 𝑥 ·Q 𝑦 ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑢 = ( 𝑓 ·Q 𝑧 ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) ) ) )
27 26 rexlimivv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑣 = ( 𝑥 ·Q 𝑦 ) → ( ( 𝑓 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑢 = ( 𝑓 ·Q 𝑧 ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) ) )
28 27 rexlimdvv ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑣 = ( 𝑥 ·Q 𝑦 ) → ( ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) → ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) )
29 28 com3r ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑣 = ( 𝑥 ·Q 𝑦 ) → ( ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) )
30 15 29 sylbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) → ( ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) ) )
31 30 impd ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∧ ∃ 𝑓 ∈ 𝐴 ∃ 𝑧 ∈ 𝐶 𝑢 = ( 𝑓 ·Q 𝑧 ) ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) )
32 12 31 sylbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 ·P 𝐶 ) ) → ( 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) ) )
33 32 rexlimdvv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ∃ 𝑣 ∈ ( 𝐴 ·P 𝐵 ) ∃ 𝑢 ∈ ( 𝐴 ·P 𝐶 ) 𝑤 = ( 𝑣 +Q 𝑢 ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
34 7 33 sylbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 ∈ ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) → 𝑤 ∈ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) ) )
35 34 ssrdv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝐴 ·P 𝐵 ) +P ( 𝐴 ·P 𝐶 ) ) ⊆ ( 𝐴 ·P ( 𝐵 +P 𝐶 ) ) )