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 \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C) \subseteq A \cdot_{𝑷} (B +_{𝑷} C)$

Proof

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

Metamath Proof Explorer

Theorem distrlem5pr

Proof