Metamath Proof Explorer

Theorem islssfg2

Description: Property of a finitely generated left (sub)module, with a relaxed constraint on the spanning vectors. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Hypotheses islssfg.x 
|- X = ( W |`s U )
islssfg.s 
|- S = ( LSubSp ` W )
islssfg.n 
|- N = ( LSpan ` W )
islssfg2.b 
|- B = ( Base ` W )
Assertion islssfg2 
|- ( ( W e. LMod /\ U e. S ) -> ( X e. LFinGen <-> E. b e. ( ~P B i^i Fin ) ( N ` b ) = U ) )

Proof

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 ) )