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 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C ⊆ A ⋅ 𝑷 B + 𝑷 C

Proof

Step Hyp Ref Expression
1 mulclpr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⋅ 𝑷 B ∈ 𝑷
2 1 3adant3 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B ∈ 𝑷
3 mulclpr ⊢ A ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 C ∈ 𝑷
4 df-plp ⊢ + 𝑷 = x ∈ 𝑷 , y ∈ 𝑷 ⟼ f | ∃ g ∈ x ∃ h ∈ y f = g + 𝑸 h
5 addclnq ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → g + 𝑸 h ∈ 𝑸
6 4 5 genpelv ⊢ A ⋅ 𝑷 B ∈ 𝑷 ∧ A ⋅ 𝑷 C ∈ 𝑷 → w ∈ A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C ↔ ∃ v ∈ A ⋅ 𝑷 B ∃ u ∈ A ⋅ 𝑷 C w = v + 𝑸 u
7 2 3 6 3imp3i2an ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w ∈ A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C ↔ ∃ v ∈ A ⋅ 𝑷 B ∃ u ∈ A ⋅ 𝑷 C w = v + 𝑸 u
8 df-mp ⊢ ⋅ 𝑷 = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ g ∈ w ∃ h ∈ v x = g ⋅ 𝑸 h
9 mulclnq ⊢ g ∈ 𝑸 ∧ h ∈ 𝑸 → g ⋅ 𝑸 h ∈ 𝑸
10 8 9 genpelv ⊢ A ∈ 𝑷 ∧ C ∈ 𝑷 → u ∈ A ⋅ 𝑷 C ↔ ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z
11 10 3adant2 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → u ∈ A ⋅ 𝑷 C ↔ ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z
12 11 anbi2d ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → v ∈ A ⋅ 𝑷 B ∧ u ∈ A ⋅ 𝑷 C ↔ v ∈ A ⋅ 𝑷 B ∧ ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z
13 df-mp ⊢ ⋅ 𝑷 = w ∈ 𝑷 , v ∈ 𝑷 ⟼ f | ∃ g ∈ w ∃ h ∈ v f = g ⋅ 𝑸 h
14 13 9 genpelv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → v ∈ A ⋅ 𝑷 B ↔ ∃ x ∈ A ∃ y ∈ B v = x ⋅ 𝑸 y
15 14 3adant3 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → v ∈ A ⋅ 𝑷 B ↔ ∃ x ∈ A ∃ y ∈ B v = x ⋅ 𝑸 y
16 distrlem4pr ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ x ∈ A ∧ y ∈ B ∧ f ∈ A ∧ z ∈ C → x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z ∈ A ⋅ 𝑷 B + 𝑷 C
17 oveq12 ⊢ v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z → v + 𝑸 u = x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z
18 17 eqeq2d ⊢ v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z → w = v + 𝑸 u ↔ w = x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z
19 eleq1 ⊢ w = x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z → w ∈ A ⋅ 𝑷 B + 𝑷 C ↔ x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z ∈ A ⋅ 𝑷 B + 𝑷 C
20 18 19 syl6bi ⊢ v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C ↔ x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z ∈ A ⋅ 𝑷 B + 𝑷 C
21 20 imp ⊢ v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z ∧ w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C ↔ x ⋅ 𝑸 y + 𝑸 f ⋅ 𝑸 z ∈ A ⋅ 𝑷 B + 𝑷 C
22 16 21 syl5ibrcom ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 ∧ x ∈ A ∧ y ∈ B ∧ f ∈ A ∧ z ∈ C → v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z ∧ w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
23 22 exp4b ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → x ∈ A ∧ y ∈ B ∧ f ∈ A ∧ z ∈ C → v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
24 23 com3l ⊢ x ∈ A ∧ y ∈ B ∧ f ∈ A ∧ z ∈ C → v = x ⋅ 𝑸 y ∧ u = f ⋅ 𝑸 z → A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
25 24 exp4b ⊢ x ∈ A ∧ y ∈ B → f ∈ A ∧ z ∈ C → v = x ⋅ 𝑸 y → u = f ⋅ 𝑸 z → A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
26 25 com23 ⊢ x ∈ A ∧ y ∈ B → v = x ⋅ 𝑸 y → f ∈ A ∧ z ∈ C → u = f ⋅ 𝑸 z → A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
27 26 rexlimivv ⊢ ∃ x ∈ A ∃ y ∈ B v = x ⋅ 𝑸 y → f ∈ A ∧ z ∈ C → u = f ⋅ 𝑸 z → A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
28 27 rexlimdvv ⊢ ∃ x ∈ A ∃ y ∈ B v = x ⋅ 𝑸 y → ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z → A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
29 28 com3r ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ x ∈ A ∃ y ∈ B v = x ⋅ 𝑸 y → ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
30 15 29 sylbid ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → v ∈ A ⋅ 𝑷 B → ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
31 30 impd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → v ∈ A ⋅ 𝑷 B ∧ ∃ f ∈ A ∃ z ∈ C u = f ⋅ 𝑸 z → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
32 12 31 sylbid ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → v ∈ A ⋅ 𝑷 B ∧ u ∈ A ⋅ 𝑷 C → w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
33 32 rexlimdvv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → ∃ v ∈ A ⋅ 𝑷 B ∃ u ∈ A ⋅ 𝑷 C w = v + 𝑸 u → w ∈ A ⋅ 𝑷 B + 𝑷 C
34 7 33 sylbid ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → w ∈ A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C → w ∈ A ⋅ 𝑷 B + 𝑷 C
35 34 ssrdv ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ C ∈ 𝑷 → A ⋅ 𝑷 B + 𝑷 A ⋅ 𝑷 C ⊆ A ⋅ 𝑷 B + 𝑷 C