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