reclem4pr

Description: Lemma for Proposition 9-3.7(v) of Gleason p. 124. (Contributed by NM, 30-Apr-1996) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	reclempr.1	$⊢ B = \{x \| \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\}$
	Assertion	reclem4pr	$⊢ A \in 𝑷 \to A \cdot_{𝑷} B = 1_{𝑷}$

Proof

Step	Hyp	Ref	Expression
1		reclempr.1	$⊢ B = \{x \| \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\}$
2	1	reclem2pr	$⊢ A \in 𝑷 \to B \in 𝑷$
3		df-mp	$⊢ \cdot_{𝑷} = (y \in 𝑷, w \in 𝑷 ⟼ \{u \| \exists f \in y \exists g \in w u = f \cdot_{𝑸} g\})$
4		mulclnq	$⊢ (f \in 𝑸 \land g \in 𝑸) \to f \cdot_{𝑸} g \in 𝑸$
5	3 4	genpelv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to (w \in (A \cdot_{𝑷} B) \leftrightarrow \exists z \in A \exists x \in B w = z \cdot_{𝑸} x)$
6	2 5	mpdan	$⊢ A \in 𝑷 \to (w \in (A \cdot_{𝑷} B) \leftrightarrow \exists z \in A \exists x \in B w = z \cdot_{𝑸} x)$
7	1	abeq2i	$⊢ x \in B \leftrightarrow \exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A)$
8		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
9	8	brel	$⊢ x <_{𝑸} y \to (x \in 𝑸 \land y \in 𝑸)$
10	9	simprd	$⊢ x <_{𝑸} y \to y \in 𝑸$
11		elprnq	$⊢ (A \in 𝑷 \land z \in A) \to z \in 𝑸$
12		ltmnq	$⊢ z \in 𝑸 \to (x <_{𝑸} y \leftrightarrow (z \cdot_{𝑸} x) <_{𝑸} (z \cdot_{𝑸} y))$
13	11 12	syl	$⊢ (A \in 𝑷 \land z \in A) \to (x <_{𝑸} y \leftrightarrow (z \cdot_{𝑸} x) <_{𝑸} (z \cdot_{𝑸} y))$
14	13	biimpd	$⊢ (A \in 𝑷 \land z \in A) \to (x <_{𝑸} y \to (z \cdot_{𝑸} x) <_{𝑸} (z \cdot_{𝑸} y))$
15	14	adantr	$⊢ ((A \in 𝑷 \land z \in A) \land y \in 𝑸) \to (x <_{𝑸} y \to (z \cdot_{𝑸} x) <_{𝑸} (z \cdot_{𝑸} y))$
16		recclnq	$⊢ y \in 𝑸 \to *_{𝑸} (y) \in 𝑸$
17		prub	$⊢ ((A \in 𝑷 \land z \in A) \land _{𝑸} (y) \in 𝑸) \to (\neg _{𝑸} (y) \in A \to z <_{𝑸} *_{𝑸} (y))$
18	16 17	sylan2	$⊢ ((A \in 𝑷 \land z \in A) \land y \in 𝑸) \to (\neg _{𝑸} (y) \in A \to z <_{𝑸} _{𝑸} (y))$
19		ltmnq	$⊢ y \in 𝑸 \to (z <_{𝑸} _{𝑸} (y) \leftrightarrow (y \cdot_{𝑸} z) <_{𝑸} (y \cdot_{𝑸} _{𝑸} (y)))$
20		mulcomnq	$⊢ y \cdot_{𝑸} z = z \cdot_{𝑸} y$
21	20	a1i	$⊢ y \in 𝑸 \to y \cdot_{𝑸} z = z \cdot_{𝑸} y$
22		recidnq	$⊢ y \in 𝑸 \to y \cdot_{𝑸} *_{𝑸} (y) = 1_{𝑸}$
23	21 22	breq12d	$⊢ y \in 𝑸 \to ((y \cdot_{𝑸} z) <_{𝑸} (y \cdot_{𝑸} *_{𝑸} (y)) \leftrightarrow (z \cdot_{𝑸} y) <_{𝑸} 1_{𝑸})$
24	19 23	bitrd	$⊢ y \in 𝑸 \to (z <_{𝑸} *_{𝑸} (y) \leftrightarrow (z \cdot_{𝑸} y) <_{𝑸} 1_{𝑸})$
25	24	adantl	$⊢ ((A \in 𝑷 \land z \in A) \land y \in 𝑸) \to (z <_{𝑸} *_{𝑸} (y) \leftrightarrow (z \cdot_{𝑸} y) <_{𝑸} 1_{𝑸})$
26	18 25	sylibd	$⊢ ((A \in 𝑷 \land z \in A) \land y \in 𝑸) \to (\neg *_{𝑸} (y) \in A \to (z \cdot_{𝑸} y) <_{𝑸} 1_{𝑸})$
27	15 26	anim12d	$⊢ ((A \in 𝑷 \land z \in A) \land y \in 𝑸) \to ((x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to ((z \cdot_{𝑸} x) <_{𝑸} (z \cdot_{𝑸} y) \land (z \cdot_{𝑸} y) <_{𝑸} 1_{𝑸}))$
28		ltsonq	$⊢ <_{𝑸} Or 𝑸$
29	28 8	sotri	$⊢ ((z \cdot_{𝑸} x) <_{𝑸} (z \cdot_{𝑸} y) \land (z \cdot_{𝑸} y) <_{𝑸} 1_{𝑸}) \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸}$
30	27 29	syl6	$⊢ ((A \in 𝑷 \land z \in A) \land y \in 𝑸) \to ((x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})$
31	30	exp4b	$⊢ (A \in 𝑷 \land z \in A) \to (y \in 𝑸 \to (x <_{𝑸} y \to (\neg *_{𝑸} (y) \in A \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})))$
32	10 31	syl5	$⊢ (A \in 𝑷 \land z \in A) \to (x <_{𝑸} y \to (x <_{𝑸} y \to (\neg *_{𝑸} (y) \in A \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})))$
33	32	pm2.43d	$⊢ (A \in 𝑷 \land z \in A) \to (x <_{𝑸} y \to (\neg *_{𝑸} (y) \in A \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸}))$
34	33	impd	$⊢ (A \in 𝑷 \land z \in A) \to ((x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})$
35	34	exlimdv	$⊢ (A \in 𝑷 \land z \in A) \to (\exists y (x <_{𝑸} y \land \neg *_{𝑸} (y) \in A) \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})$
36	7 35	syl5bi	$⊢ (A \in 𝑷 \land z \in A) \to (x \in B \to (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})$
37		breq1	$⊢ w = z \cdot_{𝑸} x \to (w <_{𝑸} 1_{𝑸} \leftrightarrow (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸})$
38	37	biimprcd	$⊢ (z \cdot_{𝑸} x) <_{𝑸} 1_{𝑸} \to (w = z \cdot_{𝑸} x \to w <_{𝑸} 1_{𝑸})$
39	36 38	syl6	$⊢ (A \in 𝑷 \land z \in A) \to (x \in B \to (w = z \cdot_{𝑸} x \to w <_{𝑸} 1_{𝑸}))$
40	39	expimpd	$⊢ A \in 𝑷 \to ((z \in A \land x \in B) \to (w = z \cdot_{𝑸} x \to w <_{𝑸} 1_{𝑸}))$
41	40	rexlimdvv	$⊢ A \in 𝑷 \to (\exists z \in A \exists x \in B w = z \cdot_{𝑸} x \to w <_{𝑸} 1_{𝑸})$
42	6 41	sylbid	$⊢ A \in 𝑷 \to (w \in (A \cdot_{𝑷} B) \to w <_{𝑸} 1_{𝑸})$
43		df-1p	$⊢ 1_{𝑷} = \{w \| w <_{𝑸} 1_{𝑸}\}$
44	43	abeq2i	$⊢ w \in 1_{𝑷} \leftrightarrow w <_{𝑸} 1_{𝑸}$
45	42 44	syl6ibr	$⊢ A \in 𝑷 \to (w \in (A \cdot_{𝑷} B) \to w \in 1_{𝑷})$
46	45	ssrdv	$⊢ A \in 𝑷 \to A \cdot_{𝑷} B \subseteq 1_{𝑷}$
47	1	reclem3pr	$⊢ A \in 𝑷 \to 1_{𝑷} \subseteq A \cdot_{𝑷} B$
48	46 47	eqssd	$⊢ A \in 𝑷 \to A \cdot_{𝑷} B = 1_{𝑷}$

Metamath Proof Explorer

Theorem reclem4pr

Proof