addclprlem2

Description: Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of Gleason p. 123. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	addclprlem2	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to x \in (A +_{𝑷} B))$

Proof

Step	Hyp	Ref	Expression
1		addclprlem1	$⊢ ((A \in 𝑷 \land g \in A) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to (x \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g \in A)$
2	1	adantlr	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to (x \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g \in A)$
3		addclprlem1	$⊢ ((B \in 𝑷 \land h \in B) \land x \in 𝑸) \to (x <_{𝑸} (h +_{𝑸} g) \to (x \cdot_{𝑸} *_{𝑸} (h +_{𝑸} g)) \cdot_{𝑸} h \in B)$
4		addcomnq	$⊢ g +_{𝑸} h = h +_{𝑸} g$
5	4	breq2i	$⊢ x <_{𝑸} (g +_{𝑸} h) \leftrightarrow x <_{𝑸} (h +_{𝑸} g)$
6	4	fveq2i	$⊢ _{𝑸} (g +_{𝑸} h) = _{𝑸} (h +_{𝑸} g)$
7	6	oveq2i	$⊢ x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h) = x \cdot_{𝑸} _{𝑸} (h +_{𝑸} g)$
8	7	oveq1i	$⊢ (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h = (x \cdot_{𝑸} _{𝑸} (h +_{𝑸} g)) \cdot_{𝑸} h$
9	8	eleq1i	$⊢ (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h \in B \leftrightarrow (x \cdot_{𝑸} _{𝑸} (h +_{𝑸} g)) \cdot_{𝑸} h \in B$
10	3 5 9	3imtr4g	$⊢ ((B \in 𝑷 \land h \in B) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to (x \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h \in B)$
11	10	adantll	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to (x \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h \in B)$
12	2 11	jcad	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g \in A \land (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h \in B))$
13		simpl	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B))$
14		simpl	$⊢ (A \in 𝑷 \land g \in A) \to A \in 𝑷$
15		simpl	$⊢ (B \in 𝑷 \land h \in B) \to B \in 𝑷$
16	14 15	anim12i	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to (A \in 𝑷 \land B \in 𝑷)$
17		df-plp	$⊢ +_{𝑷} = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y +_{𝑸} z\})$
18		addclnq	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y +_{𝑸} z \in 𝑸$
19	17 18	genpprecl	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g \in A \land (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h \in B) \to ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h) \in (A +_{𝑷} B))$
20	13 16 19	3syl	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g \in A \land (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h \in B) \to ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h) \in (A +_{𝑷} B))$
21	12 20	syld	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h) \in (A +_{𝑷} B))$
22		distrnq	$⊢ (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} (g +_{𝑸} h) = ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h)$
23		mulassnq	$⊢ (x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} (g +_{𝑸} h) = x \cdot_{𝑸} (_{𝑸} (g +_{𝑸} h) \cdot_{𝑸} (g +_{𝑸} h))$
24	22 23	eqtr3i	$⊢ ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h) = x \cdot_{𝑸} (*_{𝑸} (g +_{𝑸} h) \cdot_{𝑸} (g +_{𝑸} h))$
25		mulcomnq	$⊢ _{𝑸} (g +_{𝑸} h) \cdot_{𝑸} (g +_{𝑸} h) = (g +_{𝑸} h) \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)$
26		elprnq	$⊢ (A \in 𝑷 \land g \in A) \to g \in 𝑸$
27		elprnq	$⊢ (B \in 𝑷 \land h \in B) \to h \in 𝑸$
28	26 27	anim12i	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to (g \in 𝑸 \land h \in 𝑸)$
29		addclnq	$⊢ (g \in 𝑸 \land h \in 𝑸) \to g +_{𝑸} h \in 𝑸$
30		recidnq	$⊢ g +_{𝑸} h \in 𝑸 \to (g +_{𝑸} h) \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h) = 1_{𝑸}$
31	28 29 30	3syl	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to (g +_{𝑸} h) \cdot_{𝑸} *_{𝑸} (g +_{𝑸} h) = 1_{𝑸}$
32	25 31	eqtrid	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to *_{𝑸} (g +_{𝑸} h) \cdot_{𝑸} (g +_{𝑸} h) = 1_{𝑸}$
33	32	oveq2d	$⊢ ((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \to x \cdot_{𝑸} (*_{𝑸} (g +_{𝑸} h) \cdot_{𝑸} (g +_{𝑸} h)) = x \cdot_{𝑸} 1_{𝑸}$
34		mulidnq	$⊢ x \in 𝑸 \to x \cdot_{𝑸} 1_{𝑸} = x$
35	33 34	sylan9eq	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to x \cdot_{𝑸} (*_{𝑸} (g +_{𝑸} h) \cdot_{𝑸} (g +_{𝑸} h)) = x$
36	24 35	eqtrid	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h) = x$
37	36	eleq1d	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} g) +_{𝑸} ((x \cdot_{𝑸} _{𝑸} (g +_{𝑸} h)) \cdot_{𝑸} h) \in (A +_{𝑷} B) \leftrightarrow x \in (A +_{𝑷} B))$
38	21 37	sylibd	$⊢ (((A \in 𝑷 \land g \in A) \land (B \in 𝑷 \land h \in B)) \land x \in 𝑸) \to (x <_{𝑸} (g +_{𝑸} h) \to x \in (A +_{𝑷} B))$

Metamath Proof Explorer

Theorem addclprlem2

Proof