Metamath Proof Explorer

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 abeq2i ⊢ ( 𝑤 ∈ 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 syl5bb ⊢ ( 𝑤 ∈ 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 syl5bi ⊢ ( 𝐴 ∈ P → ( 𝑤 ∈ 1P → 𝑤 ∈ ( 𝐴 ·P 𝐵 ) ) )
105 104 ssrdv ⊢ ( 𝐴 ∈ P → 1P ⊆ ( 𝐴 ·P 𝐵 ) )