distrlem4pr

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	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))$

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((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 B \in 𝑷$
2		simprlr	$⊢ ((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 y \in B$
3		elprnq	$⊢ (B \in 𝑷 \land y \in B) \to y \in 𝑸$
4	1 2 3	syl2anc	$⊢ ((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 y \in 𝑸$
5		simp1	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to A \in 𝑷$
6		simprl	$⊢ ((x \in A \land y \in B) \land (f \in A \land z \in C)) \to f \in A$
7		elprnq	$⊢ (A \in 𝑷 \land f \in A) \to f \in 𝑸$
8	5 6 7	syl2an	$⊢ ((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 f \in 𝑸$
9		simpl3	$⊢ ((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 C \in 𝑷$
10		simprrr	$⊢ ((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 z \in C$
11		elprnq	$⊢ (C \in 𝑷 \land z \in C) \to z \in 𝑸$
12	9 10 11	syl2anc	$⊢ ((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 z \in 𝑸$
13		vex	$⊢ x \in V$
14		vex	$⊢ f \in V$
15		ltmnq	$⊢ u \in 𝑸 \to (w <_{𝑸} v \leftrightarrow (u \cdot_{𝑸} w) <_{𝑸} (u \cdot_{𝑸} v))$
16		vex	$⊢ y \in V$
17		mulcomnq	$⊢ w \cdot_{𝑸} v = v \cdot_{𝑸} w$
18	13 14 15 16 17	caovord2	$⊢ y \in 𝑸 \to (x <_{𝑸} f \leftrightarrow (x \cdot_{𝑸} y) <_{𝑸} (f \cdot_{𝑸} y))$
19		mulclnq	$⊢ (f \in 𝑸 \land z \in 𝑸) \to f \cdot_{𝑸} z \in 𝑸$
20		ovex	$⊢ x \cdot_{𝑸} y \in V$
21		ovex	$⊢ f \cdot_{𝑸} y \in V$
22		ltanq	$⊢ u \in 𝑸 \to (w <_{𝑸} v \leftrightarrow (u +_{𝑸} w) <_{𝑸} (u +_{𝑸} v))$
23		ovex	$⊢ f \cdot_{𝑸} z \in V$
24		addcomnq	$⊢ w +_{𝑸} v = v +_{𝑸} w$
25	20 21 22 23 24	caovord2	$⊢ f \cdot_{𝑸} z \in 𝑸 \to ((x \cdot_{𝑸} y) <_{𝑸} (f \cdot_{𝑸} y) \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)))$
26	19 25	syl	$⊢ (f \in 𝑸 \land z \in 𝑸) \to ((x \cdot_{𝑸} y) <_{𝑸} (f \cdot_{𝑸} y) \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)))$
27	18 26	sylan9bb	$⊢ (y \in 𝑸 \land (f \in 𝑸 \land z \in 𝑸)) \to (x <_{𝑸} f \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)))$
28	4 8 12 27	syl12anc	$⊢ ((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 <_{𝑸} f \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)))$
29		simpl1	$⊢ ((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 A \in 𝑷$
30		addclpr	$⊢ (B \in 𝑷 \land C \in 𝑷) \to B +_{𝑷} C \in 𝑷$
31	30	3adant1	$⊢ (A \in 𝑷 \land B \in 𝑷 \land C \in 𝑷) \to B +_{𝑷} C \in 𝑷$
32	31	adantr	$⊢ ((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 B +_{𝑷} C \in 𝑷$
33		mulclpr	$⊢ (A \in 𝑷 \land B +_{𝑷} C \in 𝑷) \to A \cdot_{𝑷} (B +_{𝑷} C) \in 𝑷$
34	29 32 33	syl2anc	$⊢ ((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 A \cdot_{𝑷} (B +_{𝑷} C) \in 𝑷$
35		distrnq	$⊢ f \cdot_{𝑸} (y +_{𝑸} z) = (f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)$
36		simprrl	$⊢ ((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 f \in A$
37		df-plp	$⊢ +_{𝑷} = (u \in 𝑷, v \in 𝑷 ⟼ \{w \| \exists g \in u \exists h \in v w = g +_{𝑸} h\})$
38		addclnq	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g +_{𝑸} h \in 𝑸$
39	37 38	genpprecl	$⊢ (B \in 𝑷 \land C \in 𝑷) \to ((y \in B \land z \in C) \to y +_{𝑸} z \in (B +_{𝑷} C))$
40	39	imp	$⊢ ((B \in 𝑷 \land C \in 𝑷) \land (y \in B \land z \in C)) \to y +_{𝑸} z \in (B +_{𝑷} C)$
41	1 9 2 10 40	syl22anc	$⊢ ((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 y +_{𝑸} z \in (B +_{𝑷} C)$
42		df-mp	$⊢ \cdot_{𝑷} = (u \in 𝑷, v \in 𝑷 ⟼ \{w \| \exists g \in u \exists h \in v w = g \cdot_{𝑸} h\})$
43		mulclnq	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g \cdot_{𝑸} h \in 𝑸$
44	42 43	genpprecl	$⊢ (A \in 𝑷 \land B +_{𝑷} C \in 𝑷) \to ((f \in A \land y +_{𝑸} z \in (B +_{𝑷} C)) \to f \cdot_{𝑸} (y +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
45	44	imp	$⊢ ((A \in 𝑷 \land B +_{𝑷} C \in 𝑷) \land (f \in A \land y +_{𝑸} z \in (B +_{𝑷} C))) \to f \cdot_{𝑸} (y +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))$
46	29 32 36 41 45	syl22anc	$⊢ ((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 f \cdot_{𝑸} (y +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))$
47	35 46	eqeltrrid	$⊢ ((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 (f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))$
48		prcdnq	$⊢ (A \cdot_{𝑷} (B +_{𝑷} C) \in 𝑷 \land (f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))) \to (((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
49	34 47 48	syl2anc	$⊢ ((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)) <_{𝑸} ((f \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
50	28 49	sylbid	$⊢ ((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 <_{𝑸} f \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
51		simpll	$⊢ ((x \in A \land y \in B) \land (f \in A \land z \in C)) \to x \in A$
52		elprnq	$⊢ (A \in 𝑷 \land x \in A) \to x \in 𝑸$
53	5 51 52	syl2an	$⊢ ((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 \in 𝑸$
54		vex	$⊢ z \in V$
55	14 13 15 54 17	caovord2	$⊢ z \in 𝑸 \to (f <_{𝑸} x \leftrightarrow (f \cdot_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} z))$
56		mulclnq	$⊢ (x \in 𝑸 \land y \in 𝑸) \to x \cdot_{𝑸} y \in 𝑸$
57		ltanq	$⊢ x \cdot_{𝑸} y \in 𝑸 \to ((f \cdot_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} z) \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)))$
58	56 57	syl	$⊢ (x \in 𝑸 \land y \in 𝑸) \to ((f \cdot_{𝑸} z) <_{𝑸} (x \cdot_{𝑸} z) \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)))$
59	55 58	sylan9bbr	$⊢ ((x \in 𝑸 \land y \in 𝑸) \land z \in 𝑸) \to (f <_{𝑸} x \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)))$
60	53 4 12 59	syl21anc	$⊢ ((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 (f <_{𝑸} x \leftrightarrow ((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)))$
61		distrnq	$⊢ x \cdot_{𝑸} (y +_{𝑸} z) = (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)$
62		simprll	$⊢ ((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 \in A$
63	42 43	genpprecl	$⊢ (A \in 𝑷 \land B +_{𝑷} C \in 𝑷) \to ((x \in A \land y +_{𝑸} z \in (B +_{𝑷} C)) \to x \cdot_{𝑸} (y +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
64	63	imp	$⊢ ((A \in 𝑷 \land B +_{𝑷} C \in 𝑷) \land (x \in A \land y +_{𝑸} z \in (B +_{𝑷} C))) \to x \cdot_{𝑸} (y +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))$
65	29 32 62 41 64	syl22anc	$⊢ ((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 +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))$
66	61 65	eqeltrrid	$⊢ ((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) +_{𝑸} (x \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))$
67		prcdnq	$⊢ (A \cdot_{𝑷} (B +_{𝑷} C) \in 𝑷 \land (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C))) \to (((x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)) <_{𝑸} ((x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)) \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
68	34 66 67	syl2anc	$⊢ ((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)) <_{𝑸} ((x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z)) \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
69	60 68	sylbid	$⊢ ((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 (f <_{𝑸} x \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
70		ltsonq	$⊢ <_{𝑸} Or 𝑸$
71		sotrieq	$⊢ (<_{𝑸} Or 𝑸 \land (x \in 𝑸 \land f \in 𝑸)) \to (x = f \leftrightarrow \neg (x <_{𝑸} f \lor f <_{𝑸} x))$
72	70 71	mpan	$⊢ (x \in 𝑸 \land f \in 𝑸) \to (x = f \leftrightarrow \neg (x <_{𝑸} f \lor f <_{𝑸} x))$
73	53 8 72	syl2anc	$⊢ ((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 = f \leftrightarrow \neg (x <_{𝑸} f \lor f <_{𝑸} x))$
74		oveq1	$⊢ x = f \to x \cdot_{𝑸} z = f \cdot_{𝑸} z$
75	74	oveq2d	$⊢ x = f \to (x \cdot_{𝑸} y) +_{𝑸} (x \cdot_{𝑸} z) = (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)$
76	61 75	syl5eq	$⊢ x = f \to x \cdot_{𝑸} (y +_{𝑸} z) = (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z)$
77	76	eleq1d	$⊢ x = f \to (x \cdot_{𝑸} (y +_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)) \leftrightarrow (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
78	65 77	syl5ibcom	$⊢ ((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 = f \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
79	73 78	sylbird	$⊢ ((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 (\neg (x <_{𝑸} f \lor f <_{𝑸} x) \to (x \cdot_{𝑸} y) +_{𝑸} (f \cdot_{𝑸} z) \in (A \cdot_{𝑷} (B +_{𝑷} C)))$
80	50 69 79	ecase3d	$⊢ ((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))$

Metamath Proof Explorer

Theorem distrlem4pr

Proof