Theorem reclem3pr

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

	Ref	Expression
Hypothesis	reclempr.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
Assertion	reclem3pr	⊢ ( 𝐴 ∈ P → 1P ⊆ ( 𝐴 ·P 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		reclempr.1	⊢ 𝐵 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
2		df-1p	⊢ 1P = { 𝑤 ∣ 𝑤 <Q 1Q }
3	2	eqabri	⊢ ( 𝑤 ∈ 1P ↔ 𝑤 <Q 1Q )
4		ltrnq	⊢ ( 𝑤 <Q 1Q ↔ ( *Q ‘ 1Q ) <Q ( *Q ‘ 𝑤 ) )
5		mulcomnq	⊢ ( ( *Q ‘ 1Q ) ·Q 1Q ) = ( 1Q ·Q ( *Q ‘ 1Q ) )
6		1nq	⊢ 1Q ∈ Q
7		recclnq	⊢ ( 1Q ∈ Q → ( *Q ‘ 1Q ) ∈ Q )
8		mulidnq	⊢ ( ( *Q ‘ 1Q ) ∈ Q → ( ( *Q ‘ 1Q ) ·Q 1Q ) = ( *Q ‘ 1Q ) )
9	6 7 8	mp2b	⊢ ( ( *Q ‘ 1Q ) ·Q 1Q ) = ( *Q ‘ 1Q )
10		recidnq	⊢ ( 1Q ∈ Q → ( 1Q ·Q ( *Q ‘ 1Q ) ) = 1Q )
11	6 10	ax-mp	⊢ ( 1Q ·Q ( *Q ‘ 1Q ) ) = 1Q
12	5 9 11	3eqtr3i	⊢ ( *Q ‘ 1Q ) = 1Q
13	12	breq1i	⊢ ( ( *Q ‘ 1Q ) <Q ( *Q ‘ 𝑤 ) ↔ 1Q <Q ( *Q ‘ 𝑤 ) )
14	4 13	bitri	⊢ ( 𝑤 <Q 1Q ↔ 1Q <Q ( *Q ‘ 𝑤 ) )
15		prlem936	⊢ ( ( 𝐴 ∈ P ∧ 1Q <Q ( *Q ‘ 𝑤 ) ) → ∃ 𝑣 ∈ 𝐴 ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 )
16	14 15	sylan2b	⊢ ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) → ∃ 𝑣 ∈ 𝐴 ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 )
17		prnmax	⊢ ( ( 𝐴 ∈ P ∧ 𝑣 ∈ 𝐴 ) → ∃ 𝑧 ∈ 𝐴 𝑣 <Q 𝑧 )
18	17	ad2ant2r	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ 𝐴 𝑣 <Q 𝑧 )
19		elprnq	⊢ ( ( 𝐴 ∈ P ∧ 𝑣 ∈ 𝐴 ) → 𝑣 ∈ Q )
20	19	ad2ant2r	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → 𝑣 ∈ Q )
21	20	3adant3	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → 𝑣 ∈ Q )
22		simp1r	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → 𝑤 <Q 1Q )
23		ltrelnq	⊢ <Q ⊆ ( Q × Q )
24	23	brel	⊢ ( 𝑤 <Q 1Q → ( 𝑤 ∈ Q ∧ 1Q ∈ Q ) )
25	24	simpld	⊢ ( 𝑤 <Q 1Q → 𝑤 ∈ Q )
26	22 25	syl	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → 𝑤 ∈ Q )
27		simp3	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → 𝑣 <Q 𝑧 )
28		simp2r	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 )
29		ltrnq	⊢ ( 𝑣 <Q 𝑧 ↔ ( *Q ‘ 𝑧 ) <Q ( *Q ‘ 𝑣 ) )
30		fvex	⊢ ( *Q ‘ 𝑧 ) ∈ V
31		fvex	⊢ ( *Q ‘ 𝑣 ) ∈ V
32		ltmnq	⊢ ( 𝑢 ∈ Q → ( 𝑥 <Q 𝑦 ↔ ( 𝑢 ·Q 𝑥 ) <Q ( 𝑢 ·Q 𝑦 ) ) )
33		vex	⊢ 𝑤 ∈ V
34		mulcomnq	⊢ ( 𝑥 ·Q 𝑦 ) = ( 𝑦 ·Q 𝑥 )
35	30 31 32 33 34	caovord2	⊢ ( 𝑤 ∈ Q → ( ( *Q ‘ 𝑧 ) <Q ( *Q ‘ 𝑣 ) ↔ ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) )
36	29 35	bitrid	⊢ ( 𝑤 ∈ Q → ( 𝑣 <Q 𝑧 ↔ ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) )
37	36	adantl	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( 𝑣 <Q 𝑧 ↔ ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) )
38	37	biimpd	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( 𝑣 <Q 𝑧 → ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) )
39		mulcomnq	⊢ ( 𝑣 ·Q ( *Q ‘ 𝑣 ) ) = ( ( *Q ‘ 𝑣 ) ·Q 𝑣 )
40		recidnq	⊢ ( 𝑣 ∈ Q → ( 𝑣 ·Q ( *Q ‘ 𝑣 ) ) = 1Q )
41	39 40	eqtr3id	⊢ ( 𝑣 ∈ Q → ( ( *Q ‘ 𝑣 ) ·Q 𝑣 ) = 1Q )
42		recidnq	⊢ ( 𝑤 ∈ Q → ( 𝑤 ·Q ( *Q ‘ 𝑤 ) ) = 1Q )
43	41 42	oveqan12d	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( ( *Q ‘ 𝑣 ) ·Q 𝑣 ) ·Q ( 𝑤 ·Q ( *Q ‘ 𝑤 ) ) ) = ( 1Q ·Q 1Q ) )
44		vex	⊢ 𝑣 ∈ V
45		mulassnq	⊢ ( ( 𝑥 ·Q 𝑦 ) ·Q 𝑢 ) = ( 𝑥 ·Q ( 𝑦 ·Q 𝑢 ) )
46		fvex	⊢ ( *Q ‘ 𝑤 ) ∈ V
47	31 44 33 34 45 46	caov4	⊢ ( ( ( *Q ‘ 𝑣 ) ·Q 𝑣 ) ·Q ( 𝑤 ·Q ( *Q ‘ 𝑤 ) ) ) = ( ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ·Q ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) )
48		mulidnq	⊢ ( 1Q ∈ Q → ( 1Q ·Q 1Q ) = 1Q )
49	6 48	ax-mp	⊢ ( 1Q ·Q 1Q ) = 1Q
50	43 47 49	3eqtr3g	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ·Q ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ) = 1Q )
51		recclnq	⊢ ( 𝑣 ∈ Q → ( *Q ‘ 𝑣 ) ∈ Q )
52		mulclnq	⊢ ( ( ( *Q ‘ 𝑣 ) ∈ Q ∧ 𝑤 ∈ Q ) → ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∈ Q )
53	51 52	sylan	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∈ Q )
54		recmulnq	⊢ ( ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∈ Q → ( ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) = ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ↔ ( ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ·Q ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ) = 1Q ) )
55	53 54	syl	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) = ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ↔ ( ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ·Q ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ) = 1Q ) )
56	50 55	mpbird	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) = ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) )
57	56	eleq1d	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ↔ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) )
58	57	notbid	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ↔ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) )
59	58	biimprd	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 → ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) )
60	38 59	anim12d	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( 𝑣 <Q 𝑧 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) → ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∧ ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) ) )
61		ovex	⊢ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∈ V
62		breq2	⊢ ( 𝑦 = ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) → ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ↔ ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) )
63		fveq2	⊢ ( 𝑦 = ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) → ( *Q ‘ 𝑦 ) = ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) )
64	63	eleq1d	⊢ ( 𝑦 = ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) → ( ( *Q ‘ 𝑦 ) ∈ 𝐴 ↔ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) )
65	64	notbid	⊢ ( 𝑦 = ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) → ( ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ↔ ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) )
66	62 65	anbi12d	⊢ ( 𝑦 = ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) → ( ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ↔ ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∧ ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) ) )
67	61 66	spcev	⊢ ( ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∧ ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) → ∃ 𝑦 ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) )
68		ovex	⊢ ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ V
69		breq1	⊢ ( 𝑥 = ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) → ( 𝑥 <Q 𝑦 ↔ ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ) )
70	69	anbi1d	⊢ ( 𝑥 = ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) → ( ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ↔ ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ) )
71	70	exbidv	⊢ ( 𝑥 = ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) → ( ∃ 𝑦 ( 𝑥 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ↔ ∃ 𝑦 ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ) )
72	68 71 1	elab2	⊢ ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ 𝐵 ↔ ∃ 𝑦 ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) )
73	67 72	sylibr	⊢ ( ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) <Q ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ∧ ¬ ( *Q ‘ ( ( *Q ‘ 𝑣 ) ·Q 𝑤 ) ) ∈ 𝐴 ) → ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ 𝐵 )
74	60 73	syl6	⊢ ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) → ( ( 𝑣 <Q 𝑧 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) → ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ 𝐵 ) )
75	74	imp	⊢ ( ( ( 𝑣 ∈ Q ∧ 𝑤 ∈ Q ) ∧ ( 𝑣 <Q 𝑧 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ 𝐵 )
76	21 26 27 28 75	syl22anc	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ 𝐵 )
77	23	brel	⊢ ( 𝑣 <Q 𝑧 → ( 𝑣 ∈ Q ∧ 𝑧 ∈ Q ) )
78	77	simprd	⊢ ( 𝑣 <Q 𝑧 → 𝑧 ∈ Q )
79	78	3ad2ant3	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → 𝑧 ∈ Q )
80		mulidnq	⊢ ( 𝑤 ∈ Q → ( 𝑤 ·Q 1Q ) = 𝑤 )
81		mulcomnq	⊢ ( 𝑤 ·Q 1Q ) = ( 1Q ·Q 𝑤 )
82	80 81	eqtr3di	⊢ ( 𝑤 ∈ Q → 𝑤 = ( 1Q ·Q 𝑤 ) )
83		recidnq	⊢ ( 𝑧 ∈ Q → ( 𝑧 ·Q ( *Q ‘ 𝑧 ) ) = 1Q )
84	83	oveq1d	⊢ ( 𝑧 ∈ Q → ( ( 𝑧 ·Q ( *Q ‘ 𝑧 ) ) ·Q 𝑤 ) = ( 1Q ·Q 𝑤 ) )
85		mulassnq	⊢ ( ( 𝑧 ·Q ( *Q ‘ 𝑧 ) ) ·Q 𝑤 ) = ( 𝑧 ·Q ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) )
86	84 85	eqtr3di	⊢ ( 𝑧 ∈ Q → ( 1Q ·Q 𝑤 ) = ( 𝑧 ·Q ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ) )
87	82 86	sylan9eqr	⊢ ( ( 𝑧 ∈ Q ∧ 𝑤 ∈ Q ) → 𝑤 = ( 𝑧 ·Q ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ) )
88	79 26 87	syl2anc	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → 𝑤 = ( 𝑧 ·Q ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ) )
89		oveq2	⊢ ( 𝑥 = ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) → ( 𝑧 ·Q 𝑥 ) = ( 𝑧 ·Q ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ) )
90	89	rspceeqv	⊢ ( ( ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ∈ 𝐵 ∧ 𝑤 = ( 𝑧 ·Q ( ( *Q ‘ 𝑧 ) ·Q 𝑤 ) ) ) → ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) )
91	76 88 90	syl2anc	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ∧ 𝑣 <Q 𝑧 ) → ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) )
92	91	3expia	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → ( 𝑣 <Q 𝑧 → ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
93	92	reximdv	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ 𝐴 𝑣 <Q 𝑧 → ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
94	1	reclem2pr	⊢ ( 𝐴 ∈ P → 𝐵 ∈ P )
95		df-mp	⊢ ·P = ( 𝑦 ∈ P , 𝑤 ∈ P ↦ { 𝑢 ∣ ∃ 𝑓 ∈ 𝑦 ∃ 𝑔 ∈ 𝑤 𝑢 = ( 𝑓 ·Q 𝑔 ) } )
96		mulclnq	⊢ ( ( 𝑓 ∈ Q ∧ 𝑔 ∈ Q ) → ( 𝑓 ·Q 𝑔 ) ∈ Q )
97	95 96	genpelv	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
98	94 97	mpdan	⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
99	98	ad2antrr	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → ( 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑥 ∈ 𝐵 𝑤 = ( 𝑧 ·Q 𝑥 ) ) )
100	93 99	sylibrd	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → ( ∃ 𝑧 ∈ 𝐴 𝑣 <Q 𝑧 → 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ) )
101	18 100	mpd	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) ∧ ( 𝑣 ∈ 𝐴 ∧ ¬ ( 𝑣 ·Q ( *Q ‘ 𝑤 ) ) ∈ 𝐴 ) ) → 𝑤 ∈ ( 𝐴 ·P 𝐵 ) )
102	16 101	rexlimddv	⊢ ( ( 𝐴 ∈ P ∧ 𝑤 <Q 1Q ) → 𝑤 ∈ ( 𝐴 ·P 𝐵 ) )
103	102	ex	⊢ ( 𝐴 ∈ P → ( 𝑤 <Q 1Q → 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ) )
104	3 103	biimtrid	⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ 1P → 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ) )
105	104	ssrdv	⊢ ( 𝐴 ∈ P → 1P ⊆ ( 𝐴 ·P 𝐵 ) )