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 ⊢ B = x | ∃ y x < 𝑸 y ∧ ¬ * 𝑸 ⁡ y ∈ A
Assertion reclem3pr ⊢ A ∈ 𝑷 → 1 𝑷 ⊆ A ⋅ 𝑷 B

Proof

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