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=BaseS
lindfmm.c C=BaseT
Assertion lindsmm GSLMHomTG:B1-1CFBFLIndSSGFLIndST

Proof

Step Hyp Ref Expression
1 lindfmm.b B=BaseS
2 lindfmm.c C=BaseT
3 ibar FBIFLIndFSFBIFLIndFS
4 3 3ad2ant3 GSLMHomTG:B1-1CFBIFLIndFSFBIFLIndFS
5 f1oi IF:F1-1 ontoF
6 f1of IF:F1-1 ontoFIF:FF
7 5 6 ax-mp IF:FF
8 simp3 GSLMHomTG:B1-1CFBFB
9 fss IF:FFFBIF:FB
10 7 8 9 sylancr GSLMHomTG:B1-1CFBIF:FB
11 1 2 lindfmm GSLMHomTG:B1-1CIF:FBIFLIndFSGIFLIndFT
12 10 11 syld3an3 GSLMHomTG:B1-1CFBIFLIndFSGIFLIndFT
13 4 12 bitr3d GSLMHomTG:B1-1CFBFBIFLIndFSGIFLIndFT
14 lmhmlmod1 GSLMHomTSLMod
15 14 3ad2ant1 GSLMHomTG:B1-1CFBSLMod
16 1 islinds SLModFLIndSSFBIFLIndFS
17 15 16 syl GSLMHomTG:B1-1CFBFLIndSSFBIFLIndFS
18 lmhmlmod2 GSLMHomTTLMod
19 18 3ad2ant1 GSLMHomTG:B1-1CFBTLMod
20 19 adantr GSLMHomTG:B1-1CFBGFLIndSTTLMod
21 simpr GSLMHomTG:B1-1CFBGFLIndSTGFLIndST
22 f1ores G:B1-1CFBGF:F1-1 ontoGF
23 f1of1 GF:F1-1 ontoGFGF:F1-1GF
24 22 23 syl G:B1-1CFBGF:F1-1GF
25 24 3adant1 GSLMHomTG:B1-1CFBGF:F1-1GF
26 25 adantr GSLMHomTG:B1-1CFBGFLIndSTGF:F1-1GF
27 f1linds TLModGFLIndSTGF:F1-1GFGFLIndFT
28 20 21 26 27 syl3anc GSLMHomTG:B1-1CFBGFLIndSTGFLIndFT
29 df-ima GF=ranGF
30 lindfrn TLModGFLIndFTranGFLIndST
31 19 30 sylan GSLMHomTG:B1-1CFBGFLIndFTranGFLIndST
32 29 31 eqeltrid GSLMHomTG:B1-1CFBGFLIndFTGFLIndST
33 28 32 impbida GSLMHomTG:B1-1CFBGFLIndSTGFLIndFT
34 coires1 GIF=GF
35 34 breq1i GIFLIndFTGFLIndFT
36 33 35 bitr4di GSLMHomTG:B1-1CFBGFLIndSTGIFLIndFT
37 13 17 36 3bitr4d GSLMHomTG:B1-1CFBFLIndSSGFLIndST