Step |
Hyp |
Ref |
Expression |
1 |
|
lnrfg.s |
|- S = ( Scalar ` M ) |
2 |
|
eqid |
|- ( S freeLMod a ) = ( S freeLMod a ) |
3 |
|
eqid |
|- ( Base ` ( S freeLMod a ) ) = ( Base ` ( S freeLMod a ) ) |
4 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
5 |
|
eqid |
|- ( .s ` M ) = ( .s ` M ) |
6 |
|
eqid |
|- ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) |
7 |
|
fglmod |
|- ( M e. LFinGen -> M e. LMod ) |
8 |
7
|
ad3antrrr |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> M e. LMod ) |
9 |
|
vex |
|- a e. _V |
10 |
9
|
a1i |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> a e. _V ) |
11 |
1
|
a1i |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> S = ( Scalar ` M ) ) |
12 |
|
f1oi |
|- ( _I |` a ) : a -1-1-onto-> a |
13 |
|
f1of |
|- ( ( _I |` a ) : a -1-1-onto-> a -> ( _I |` a ) : a --> a ) |
14 |
12 13
|
ax-mp |
|- ( _I |` a ) : a --> a |
15 |
|
elpwi |
|- ( a e. ~P ( Base ` M ) -> a C_ ( Base ` M ) ) |
16 |
|
fss |
|- ( ( ( _I |` a ) : a --> a /\ a C_ ( Base ` M ) ) -> ( _I |` a ) : a --> ( Base ` M ) ) |
17 |
14 15 16
|
sylancr |
|- ( a e. ~P ( Base ` M ) -> ( _I |` a ) : a --> ( Base ` M ) ) |
18 |
17
|
ad2antlr |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( _I |` a ) : a --> ( Base ` M ) ) |
19 |
2 3 4 5 6 8 10 11 18
|
frlmup1 |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) e. ( ( S freeLMod a ) LMHom M ) ) |
20 |
|
simpllr |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> S e. LNoeR ) |
21 |
|
simprl |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> a e. Fin ) |
22 |
2
|
lnrfrlm |
|- ( ( S e. LNoeR /\ a e. Fin ) -> ( S freeLMod a ) e. LNoeM ) |
23 |
20 21 22
|
syl2anc |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( S freeLMod a ) e. LNoeM ) |
24 |
|
eqid |
|- ( LSpan ` M ) = ( LSpan ` M ) |
25 |
2 3 4 5 6 8 10 11 18 24
|
frlmup3 |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( ( LSpan ` M ) ` ran ( _I |` a ) ) ) |
26 |
|
rnresi |
|- ran ( _I |` a ) = a |
27 |
26
|
fveq2i |
|- ( ( LSpan ` M ) ` ran ( _I |` a ) ) = ( ( LSpan ` M ) ` a ) |
28 |
|
simprr |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) |
29 |
27 28
|
syl5eq |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ( ( LSpan ` M ) ` ran ( _I |` a ) ) = ( Base ` M ) ) |
30 |
25 29
|
eqtrd |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( Base ` M ) ) |
31 |
4
|
lnmepi |
|- ( ( ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) e. ( ( S freeLMod a ) LMHom M ) /\ ( S freeLMod a ) e. LNoeM /\ ran ( b e. ( Base ` ( S freeLMod a ) ) |-> ( M gsum ( b oF ( .s ` M ) ( _I |` a ) ) ) ) = ( Base ` M ) ) -> M e. LNoeM ) |
32 |
19 23 30 31
|
syl3anc |
|- ( ( ( ( M e. LFinGen /\ S e. LNoeR ) /\ a e. ~P ( Base ` M ) ) /\ ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) -> M e. LNoeM ) |
33 |
4 24
|
islmodfg |
|- ( M e. LMod -> ( M e. LFinGen <-> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) ) |
34 |
7 33
|
syl |
|- ( M e. LFinGen -> ( M e. LFinGen <-> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) ) |
35 |
34
|
ibi |
|- ( M e. LFinGen -> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) |
36 |
35
|
adantr |
|- ( ( M e. LFinGen /\ S e. LNoeR ) -> E. a e. ~P ( Base ` M ) ( a e. Fin /\ ( ( LSpan ` M ) ` a ) = ( Base ` M ) ) ) |
37 |
32 36
|
r19.29a |
|- ( ( M e. LFinGen /\ S e. LNoeR ) -> M e. LNoeM ) |