Metamath Proof Explorer

Theorem lindsmm

Description: Linear independence of a set is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lindfmm.b 
|- B = ( Base ` S )
lindfmm.c 
|- C = ( Base ` T )
Assertion lindsmm 
|- ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( F e. ( LIndS ` S ) <-> ( G " F ) e. ( LIndS ` T ) ) )

Proof

Step Hyp Ref Expression
1 lindfmm.b 
 |-  B = ( Base ` S )
2 lindfmm.c 
 |-  C = ( Base ` T )
3 ibar 
 |-  ( F C_ B -> ( ( _I |` F ) LIndF S <-> ( F C_ B /\ ( _I |` F ) LIndF S ) ) )
4 3 3ad2ant3 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( ( _I |` F ) LIndF S <-> ( F C_ B /\ ( _I |` F ) LIndF S ) ) )
5 f1oi 
 |-  ( _I |` F ) : F -1-1-onto-> F
6 f1of 
 |-  ( ( _I |` F ) : F -1-1-onto-> F -> ( _I |` F ) : F --> F )
7 5 6 ax-mp 
 |-  ( _I |` F ) : F --> F
8 simp3 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> F C_ B )
9 fss 
 |-  ( ( ( _I |` F ) : F --> F /\ F C_ B ) -> ( _I |` F ) : F --> B )
10 7 8 9 sylancr 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( _I |` F ) : F --> B )
11 1 2 lindfmm 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ ( _I |` F ) : F --> B ) -> ( ( _I |` F ) LIndF S <-> ( G o. ( _I |` F ) ) LIndF T ) )
12 10 11 syld3an3 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( ( _I |` F ) LIndF S <-> ( G o. ( _I |` F ) ) LIndF T ) )
13 4 12 bitr3d 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( ( F C_ B /\ ( _I |` F ) LIndF S ) <-> ( G o. ( _I |` F ) ) LIndF T ) )
14 lmhmlmod1 
 |-  ( G e. ( S LMHom T ) -> S e. LMod )
15 14 3ad2ant1 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> S e. LMod )
16 1 islinds 
 |-  ( S e. LMod -> ( F e. ( LIndS ` S ) <-> ( F C_ B /\ ( _I |` F ) LIndF S ) ) )
17 15 16 syl 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( F e. ( LIndS ` S ) <-> ( F C_ B /\ ( _I |` F ) LIndF S ) ) )
18 lmhmlmod2 
 |-  ( G e. ( S LMHom T ) -> T e. LMod )
19 18 3ad2ant1 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> T e. LMod )
20 19 adantr 
 |-  ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) /\ ( G " F ) e. ( LIndS ` T ) ) -> T e. LMod )
21 simpr 
 |-  ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) /\ ( G " F ) e. ( LIndS ` T ) ) -> ( G " F ) e. ( LIndS ` T ) )
22 f1ores 
 |-  ( ( G : B -1-1-> C /\ F C_ B ) -> ( G |` F ) : F -1-1-onto-> ( G " F ) )
23 f1of1 
 |-  ( ( G |` F ) : F -1-1-onto-> ( G " F ) -> ( G |` F ) : F -1-1-> ( G " F ) )
24 22 23 syl 
 |-  ( ( G : B -1-1-> C /\ F C_ B ) -> ( G |` F ) : F -1-1-> ( G " F ) )
25 24 3adant1 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( G |` F ) : F -1-1-> ( G " F ) )
26 25 adantr 
 |-  ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) /\ ( G " F ) e. ( LIndS ` T ) ) -> ( G |` F ) : F -1-1-> ( G " F ) )
27 f1linds 
 |-  ( ( T e. LMod /\ ( G " F ) e. ( LIndS ` T ) /\ ( G |` F ) : F -1-1-> ( G " F ) ) -> ( G |` F ) LIndF T )
28 20 21 26 27 syl3anc 
 |-  ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) /\ ( G " F ) e. ( LIndS ` T ) ) -> ( G |` F ) LIndF T )
29 df-ima 
 |-  ( G " F ) = ran ( G |` F )
30 lindfrn 
 |-  ( ( T e. LMod /\ ( G |` F ) LIndF T ) -> ran ( G |` F ) e. ( LIndS ` T ) )
31 19 30 sylan 
 |-  ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) /\ ( G |` F ) LIndF T ) -> ran ( G |` F ) e. ( LIndS ` T ) )
32 29 31 eqeltrid 
 |-  ( ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) /\ ( G |` F ) LIndF T ) -> ( G " F ) e. ( LIndS ` T ) )
33 28 32 impbida 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( ( G " F ) e. ( LIndS ` T ) <-> ( G |` F ) LIndF T ) )
34 coires1 
 |-  ( G o. ( _I |` F ) ) = ( G |` F )
35 34 breq1i 
 |-  ( ( G o. ( _I |` F ) ) LIndF T <-> ( G |` F ) LIndF T )
36 33 35 bitr4di 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( ( G " F ) e. ( LIndS ` T ) <-> ( G o. ( _I |` F ) ) LIndF T ) )
37 13 17 36 3bitr4d 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( F e. ( LIndS ` S ) <-> ( G " F ) e. ( LIndS ` T ) ) )