Theorem 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	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
Assertion	reclem4pr	⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 𝐵 ) = 1P )

Proof

Step	Hyp	Ref	Expression
1		reclempr.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
2	1	reclem2pr	⊢ ( 𝐴 ∈ P → 𝐵 ∈ P )
3		df-mp	⊢ ·P = ( 𝑦 ∈ P , 𝑤 ∈ P ↦ { 𝑢 ∣ ∃ 𝑓 ∈ 𝑦 ∃ 𝑔 ∈ 𝑤 𝑢 = ( 𝑓 ·Q 𝑔 ) } )
4		mulclnq	⊢ ( ( 𝑓 ∈ Q ∧ 𝑔 ∈ Q ) → ( 𝑓 ·Q 𝑔 ) ∈ Q )
5	3 4	genpelv	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
6	2 5	mpdan	⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
7	1	abeq2i	⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) )
8		ltrelnq	⊢ <Q ⊆ ( Q × Q )
9	8	brel	⊢ ( 𝑥 <Q 𝑦 → ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) )
10	9	simprd	⊢ ( 𝑥 <Q 𝑦 → 𝑦 ∈ Q )
11		elprnq	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ Q )
12		ltmnq	⊢ ( 𝑧 ∈ Q → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
13	11 12	syl	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 ↔ ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
14	13	biimpd	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 → ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
15	14	adantr	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( 𝑥 <Q 𝑦 → ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ) )
16		recclnq	⊢ ( 𝑦 ∈ Q → ( *Q ‘ 𝑦 ) ∈ Q )
17		prub	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ ( *Q ‘ 𝑦 ) ∈ Q ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → 𝑧 <Q ( *Q ‘ 𝑦 ) ) )
18	16 17	sylan2	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → 𝑧 <Q ( *Q ‘ 𝑦 ) ) )
19		ltmnq	⊢ ( 𝑦 ∈ Q → ( 𝑧 <Q ( *Q ‘ 𝑦 ) ↔ ( 𝑦 ·Q 𝑧 ) <Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ) )
20		mulcomnq	⊢ ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 )
21	20	a1i	⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q 𝑧 ) = ( 𝑧 ·Q 𝑦 ) )
22		recidnq	⊢ ( 𝑦 ∈ Q → ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) = 1Q )
23	21 22	breq12d	⊢ ( 𝑦 ∈ Q → ( ( 𝑦 ·Q 𝑧 ) <Q ( 𝑦 ·Q ( *Q ‘ 𝑦 ) ) ↔ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
24	19 23	bitrd	⊢ ( 𝑦 ∈ Q → ( 𝑧 <Q ( *Q ‘ 𝑦 ) ↔ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
25	24	adantl	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( 𝑧 <Q ( *Q ‘ 𝑦 ) ↔ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
26	18 25	sylibd	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑦 ) <Q 1Q ) )
27	15 26	anim12d	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ∧ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) ) )
28		ltsonq	⊢ <Q Or Q
29	28 8	sotri	⊢ ( ( ( 𝑧 ·Q 𝑥 ) <Q ( 𝑧 ·Q 𝑦 ) ∧ ( 𝑧 ·Q 𝑦 ) <Q 1Q ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q )
30	27 29	syl6	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ Q ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
31	30	exp4b	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 ∈ Q → ( 𝑥 <Q 𝑦 → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) ) ) )
32	10 31	syl5	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 → ( 𝑥 <Q 𝑦 → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) ) ) )
33	32	pm2.43d	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <Q 𝑦 → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) ) )
34	33	impd	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
35	34	exlimdv	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
36	7 35	syl5bi	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 → ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
37		breq1	⊢ ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → ( 𝑤 <Q 1Q ↔ ( 𝑧 ·Q 𝑥 ) <Q 1Q ) )
38	37	biimprcd	⊢ ( ( 𝑧 ·Q 𝑥 ) <Q 1Q → ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) )
39	36 38	syl6	⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐵 → ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) ) )
40	39	expimpd	⊢ ( 𝐴 ∈ P → ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) ) )
41	40	rexlimdvv	⊢ ( 𝐴 ∈ P → ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) → 𝑤 <Q 1Q ) )
42	6 41	sylbid	⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) → 𝑤 <Q 1Q ) )
43		df-1p	⊢ 1P = { 𝑤 ∣ 𝑤 <Q 1Q }
44	43	abeq2i	⊢ ( 𝑤 ∈ 1P ↔ 𝑤 <Q 1Q )
45	42 44	syl6ibr	⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) → 𝑤 ∈ 1P ) )
46	45	ssrdv	⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 𝐵 ) ⊆ 1P )
47	1	reclem3pr	⊢ ( 𝐴 ∈ P → 1P ⊆ ( 𝐴 ·P 𝐵 ) )
48	46 47	eqssd	⊢ ( 𝐴 ∈ P → ( 𝐴 ·P 𝐵 ) = 1P )