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

Proof

Step	Hyp	Ref	Expression
1		addclpr	$⊢ (B \in 𝑷 \land C \in 𝑷) \to B +_{𝑷} C \in 𝑷$
2		df-mp	$⊢ \cdot_{𝑷} = (y \in 𝑷, z \in 𝑷 ⟼ \{f \| \exists g \in y \exists h \in z f = g \cdot_{𝑸} h\})$
3		mulclnq	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g \cdot_{𝑸} h \in 𝑸$
4	2 3	genpelv	$⊢ (A \in 𝑷 \land B +_{𝑷} C \in 𝑷) \to (w \in (A \cdot_{𝑷} (B +_{𝑷} C)) \leftrightarrow \exists x \in A \exists v \in (B +_{𝑷} C) w = x \cdot_{𝑸} v)$
5	1 4	sylan2	$⊢ (A \in 𝑷 \land (B \in 𝑷 \land C \in 𝑷)) \to (w \in (A \cdot_{𝑷} (B +_{𝑷} C)) \leftrightarrow \exists x \in A \exists v \in (B +_{𝑷} C) w = x \cdot_{𝑸} v)$
6	5	3impb	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (w \in (A \cdot_{𝑷} (B +_{𝑷} C)) \leftrightarrow \exists x \in A \exists v \in (B +_{𝑷} C) w = x \cdot_{𝑸} v)$
7		df-plp	$⊢ +_{𝑷} = (w \in 𝑷, x \in 𝑷 ⟼ \{f \| \exists g \in w \exists h \in x f = g +_{𝑸} h\})$
8		addclnq	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g +_{𝑸} h \in 𝑸$
9	7 8	genpelv	$⊢ (B \in 𝑷 \land C \in 𝑷) \to (v \in (B +_{𝑷} C) \leftrightarrow \exists y \in B \exists z \in C v = y +_{𝑸} z)$
10	9	3adant1	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (v \in (B +_{𝑷} C) \leftrightarrow \exists y \in B \exists z \in C v = y +_{𝑸} z)$
11	10	adantr	$⊢ ((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \to (v \in (B +_{𝑷} C) \leftrightarrow \exists y \in B \exists z \in C v = y +_{𝑸} z)$
12		simprr	$⊢ ((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \to w = x \cdot_{𝑸} v$
13		simpr	$⊢ ((y \in B \land z \in C) \land v = y +_{𝑸} z) \to v = y +_{𝑸} z$
14		oveq2	$⊢ v = y +_{𝑸} z \to x \cdot_{𝑸} v = x \cdot_{𝑸} (y +_{𝑸} z)$
15	14	eqeq2d	$⊢ v = y +_{𝑸} z \to (w = x \cdot_{𝑸} v \leftrightarrow w = x \cdot_{𝑸} (y +_{𝑸} z))$
16	15	biimpac	$⊢ (w = x \cdot_{𝑸} v \land v = y +_{𝑸} z) \to w = x \cdot_{𝑸} (y +_{𝑸} z)$
17		distrnq	$⊢ x \cdot_{𝑸} (y +_{𝑸} z) = (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)$
18	16 17	eqtrdi	$⊢ (w = x \cdot_{𝑸} v \land v = y +_{𝑸} z) \to w = (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)$
19	12 13 18	syl2an	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to w = (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)$
20		mulclpr	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A \cdot_{𝑷} B \in 𝑷$
21	20	3adant3	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to A \cdot_{𝑷} B \in 𝑷$
22	21	ad2antrr	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to A \cdot_{𝑷} B \in 𝑷$
23		mulclpr	$⊢ (A \in 𝑷 \land C \in 𝑷) \to A \cdot_{𝑷} C \in 𝑷$
24	23	3adant2	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to A \cdot_{𝑷} C \in 𝑷$
25	24	ad2antrr	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to A \cdot_{𝑷} C \in 𝑷$
26		simpll	$⊢ ((y \in B \land z \in C) \land v = y +_{𝑸} z) \to y \in B$
27	2 3	genpprecl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ((x \in A \land y \in B) \to x \cdot_{𝑸} y \in (A \cdot_{𝑷} B))$
28	27	3adant3	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to ((x \in A \land y \in B) \to x \cdot_{𝑸} y \in (A \cdot_{𝑷} B))$
29	28	impl	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land x \in A) \land y \in B) \to x \cdot_{𝑸} y \in (A \cdot_{𝑷} B)$
30	29	adantlrr	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land y \in B) \to x \cdot_{𝑸} y \in (A \cdot_{𝑷} B)$
31	26 30	sylan2	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to x \cdot_{𝑸} y \in (A \cdot_{𝑷} B)$
32		simplr	$⊢ ((y \in B \land z \in C) \land v = y +_{𝑸} z) \to z \in C$
33	2 3	genpprecl	$⊢ (A \in 𝑷 \land C \in 𝑷) \to ((x \in A \land z \in C) \to x \cdot_{𝑸} z \in (A \cdot_{𝑷} C))$
34	33	3adant2	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to ((x \in A \land z \in C) \to x \cdot_{𝑸} z \in (A \cdot_{𝑷} C))$
35	34	impl	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land x \in A) \land z \in C) \to x \cdot_{𝑸} z \in (A \cdot_{𝑷} C)$
36	35	adantlrr	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land z \in C) \to x \cdot_{𝑸} z \in (A \cdot_{𝑷} C)$
37	32 36	sylan2	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to x \cdot_{𝑸} z \in (A \cdot_{𝑷} C)$
38	7 8	genpprecl	$⊢ (A \cdot_{𝑷} B \in 𝑷 \land A \cdot_{𝑷} C \in 𝑷) \to ((x \cdot_{𝑸} y \in (A \cdot_{𝑷} B) \land x \cdot_{𝑸} z \in (A \cdot_{𝑷} C)) \to (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z) \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))$
39	38	imp	$⊢ ((A \cdot_{𝑷} B \in 𝑷 \land A \cdot_{𝑷} C \in 𝑷) \land (x \cdot_{𝑸} y \in (A \cdot_{𝑷} B) \land x \cdot_{𝑸} z \in (A \cdot_{𝑷} C))) \to (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z) \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C))$
40	22 25 31 37 39	syl22anc	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z) \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C))$
41	19 40	eqeltrd	$⊢ (((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \land ((y \in B \land z \in C) \land v = y +_{𝑸} z)) \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C))$
42	41	exp32	$⊢ ((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \to ((y \in B \land z \in C) \to (v = y +_{𝑸} z \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C))))$
43	42	rexlimdvv	$⊢ ((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \to (\exists y \in B \exists z \in C v = y +_{𝑸} z \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))$
44	11 43	sylbid	$⊢ ((A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \land (x \in A \land w = x \cdot_{𝑸} v)) \to (v \in (B +_{𝑷} C) \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))$
45	44	exp32	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (x \in A \to (w = x \cdot_{𝑸} v \to (v \in (B +_{𝑷} C) \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))))$
46	45	com34	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (x \in A \to (v \in (B +_{𝑷} C) \to (w = x \cdot_{𝑸} v \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))))$
47	46	impd	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to ((x \in A \land v \in (B +_{𝑷} C)) \to (w = x \cdot_{𝑸} v \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C))))$
48	47	rexlimdvv	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (\exists x \in A \exists v \in (B +_{𝑷} C) w = x \cdot_{𝑸} v \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))$
49	6 48	sylbid	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to (w \in (A \cdot_{𝑷} (B +_{𝑷} C)) \to w \in ((A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)))$
50	49	ssrdv	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to A \cdot_{𝑷} (B +_{𝑷} C) \subseteq (A \cdot_{𝑷} B) +_{𝑷} (A \cdot_{𝑷} C)$

Metamath Proof Explorer

Theorem distrlem1pr

Proof