Step |
Hyp |
Ref |
Expression |
1 |
|
islssfg.x |
|- X = ( W |`s U ) |
2 |
|
islssfg.s |
|- S = ( LSubSp ` W ) |
3 |
|
islssfg.n |
|- N = ( LSpan ` W ) |
4 |
|
islssfg2.b |
|- B = ( Base ` W ) |
5 |
1 2 3
|
islssfg |
|- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) ) ) |
6 |
4 2
|
lssss |
|- ( ( N ` b ) e. S -> ( N ` b ) C_ B ) |
7 |
6
|
adantl |
|- ( ( W e. LMod /\ ( N ` b ) e. S ) -> ( N ` b ) C_ B ) |
8 |
|
sstr2 |
|- ( b C_ ( N ` b ) -> ( ( N ` b ) C_ B -> b C_ B ) ) |
9 |
7 8
|
mpan9 |
|- ( ( ( W e. LMod /\ ( N ` b ) e. S ) /\ b C_ ( N ` b ) ) -> b C_ B ) |
10 |
4 3
|
lspssid |
|- ( ( W e. LMod /\ b C_ B ) -> b C_ ( N ` b ) ) |
11 |
10
|
adantlr |
|- ( ( ( W e. LMod /\ ( N ` b ) e. S ) /\ b C_ B ) -> b C_ ( N ` b ) ) |
12 |
9 11
|
impbida |
|- ( ( W e. LMod /\ ( N ` b ) e. S ) -> ( b C_ ( N ` b ) <-> b C_ B ) ) |
13 |
|
vex |
|- b e. _V |
14 |
13
|
elpw |
|- ( b e. ~P ( N ` b ) <-> b C_ ( N ` b ) ) |
15 |
13
|
elpw |
|- ( b e. ~P B <-> b C_ B ) |
16 |
12 14 15
|
3bitr4g |
|- ( ( W e. LMod /\ ( N ` b ) e. S ) -> ( b e. ~P ( N ` b ) <-> b e. ~P B ) ) |
17 |
|
eleq1 |
|- ( ( N ` b ) = U -> ( ( N ` b ) e. S <-> U e. S ) ) |
18 |
17
|
anbi2d |
|- ( ( N ` b ) = U -> ( ( W e. LMod /\ ( N ` b ) e. S ) <-> ( W e. LMod /\ U e. S ) ) ) |
19 |
|
pweq |
|- ( ( N ` b ) = U -> ~P ( N ` b ) = ~P U ) |
20 |
19
|
eleq2d |
|- ( ( N ` b ) = U -> ( b e. ~P ( N ` b ) <-> b e. ~P U ) ) |
21 |
20
|
bibi1d |
|- ( ( N ` b ) = U -> ( ( b e. ~P ( N ` b ) <-> b e. ~P B ) <-> ( b e. ~P U <-> b e. ~P B ) ) ) |
22 |
18 21
|
imbi12d |
|- ( ( N ` b ) = U -> ( ( ( W e. LMod /\ ( N ` b ) e. S ) -> ( b e. ~P ( N ` b ) <-> b e. ~P B ) ) <-> ( ( W e. LMod /\ U e. S ) -> ( b e. ~P U <-> b e. ~P B ) ) ) ) |
23 |
16 22
|
mpbii |
|- ( ( N ` b ) = U -> ( ( W e. LMod /\ U e. S ) -> ( b e. ~P U <-> b e. ~P B ) ) ) |
24 |
23
|
com12 |
|- ( ( W e. LMod /\ U e. S ) -> ( ( N ` b ) = U -> ( b e. ~P U <-> b e. ~P B ) ) ) |
25 |
24
|
adantld |
|- ( ( W e. LMod /\ U e. S ) -> ( ( b e. Fin /\ ( N ` b ) = U ) -> ( b e. ~P U <-> b e. ~P B ) ) ) |
26 |
25
|
pm5.32rd |
|- ( ( W e. LMod /\ U e. S ) -> ( ( b e. ~P U /\ ( b e. Fin /\ ( N ` b ) = U ) ) <-> ( b e. ~P B /\ ( b e. Fin /\ ( N ` b ) = U ) ) ) ) |
27 |
|
elin |
|- ( b e. ( ~P B i^i Fin ) <-> ( b e. ~P B /\ b e. Fin ) ) |
28 |
27
|
anbi1i |
|- ( ( b e. ( ~P B i^i Fin ) /\ ( N ` b ) = U ) <-> ( ( b e. ~P B /\ b e. Fin ) /\ ( N ` b ) = U ) ) |
29 |
|
anass |
|- ( ( ( b e. ~P B /\ b e. Fin ) /\ ( N ` b ) = U ) <-> ( b e. ~P B /\ ( b e. Fin /\ ( N ` b ) = U ) ) ) |
30 |
28 29
|
bitr2i |
|- ( ( b e. ~P B /\ ( b e. Fin /\ ( N ` b ) = U ) ) <-> ( b e. ( ~P B i^i Fin ) /\ ( N ` b ) = U ) ) |
31 |
26 30
|
syl6bb |
|- ( ( W e. LMod /\ U e. S ) -> ( ( b e. ~P U /\ ( b e. Fin /\ ( N ` b ) = U ) ) <-> ( b e. ( ~P B i^i Fin ) /\ ( N ` b ) = U ) ) ) |
32 |
31
|
rexbidv2 |
|- ( ( W e. LMod /\ U e. S ) -> ( E. b e. ~P U ( b e. Fin /\ ( N ` b ) = U ) <-> E. b e. ( ~P B i^i Fin ) ( N ` b ) = U ) ) |
33 |
5 32
|
bitrd |
|- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ( ~P B i^i Fin ) ( N ` b ) = U ) ) |