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

Proof

Step Hyp Ref Expression
1 reclempr.1 ⊢B=x|∃yx<𝑸y∧¬*𝑸⁡y∈A
2 df-1p ⊢1𝑷=w|w<𝑸1𝑸
3 2 eqabri ⊢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∈Av<𝑸z
18 17 ad2ant2r ⊢A∈𝑷∧w<𝑸1𝑸∧v∈A∧¬v⋅𝑸*𝑸⁡w∈A→∃z∈Av<𝑸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 bitrid ⊢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→∃yx<𝑸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∈Bw=z⋅𝑸x
91 76 88 90 syl2anc ⊢A∈𝑷∧w<𝑸1𝑸∧v∈A∧¬v⋅𝑸*𝑸⁡w∈A∧v<𝑸z→∃x∈Bw=z⋅𝑸x
92 91 3expia ⊢A∈𝑷∧w<𝑸1𝑸∧v∈A∧¬v⋅𝑸*𝑸⁡w∈A→v<𝑸z→∃x∈Bw=z⋅𝑸x
93 92 reximdv ⊢A∈𝑷∧w<𝑸1𝑸∧v∈A∧¬v⋅𝑸*𝑸⁡w∈A→∃z∈Av<𝑸z→∃z∈A∃x∈Bw=z⋅𝑸x
94 1 reclem2pr ⊢A∈𝑷→B∈𝑷
95 df-mp ⊢⋅𝑷=y∈𝑷,w∈𝑷⟼u|∃f∈y∃g∈wu=f⋅𝑸g
96 mulclnq ⊢f∈𝑸∧g∈𝑸→f⋅𝑸g∈𝑸
97 95 96 genpelv ⊢A∈𝑷∧B∈𝑷→w∈A⋅𝑷B↔∃z∈A∃x∈Bw=z⋅𝑸x
98 94 97 mpdan ⊢A∈𝑷→w∈A⋅𝑷B↔∃z∈A∃x∈Bw=z⋅𝑸x
99 98 ad2antrr ⊢A∈𝑷∧w<𝑸1𝑸∧v∈A∧¬v⋅𝑸*𝑸⁡w∈A→w∈A⋅𝑷B↔∃z∈A∃x∈Bw=z⋅𝑸x
100 93 99 sylibrd ⊢A∈𝑷∧w<𝑸1𝑸∧v∈A∧¬v⋅𝑸*𝑸⁡w∈A→∃z∈Av<𝑸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 biimtrid ⊢A∈𝑷→w∈1𝑷→w∈A⋅𝑷B
105 104 ssrdv ⊢A∈𝑷→1𝑷⊆A⋅𝑷B