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 S LMHom T G : B 1-1 C F B F LIndS S G F LIndS T

Proof

Step Hyp Ref Expression
1 lindfmm.b B = Base S
2 lindfmm.c C = Base T
3 ibar F B I F LIndF S F B I F LIndF S
4 3 3ad2ant3 G S LMHom T G : B 1-1 C F B I F LIndF S F 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 S LMHom T G : B 1-1 C F B F B
9 fss I F : F F F B I F : F B
10 7 8 9 sylancr G S LMHom T G : B 1-1 C F B I F : F B
11 1 2 lindfmm G S LMHom T G : B 1-1 C I F : F B I F LIndF S G I F LIndF T
12 10 11 syld3an3 G S LMHom T G : B 1-1 C F B I F LIndF S G I F LIndF T
13 4 12 bitr3d G S LMHom T G : B 1-1 C F B F B I F LIndF S G I F LIndF T
14 lmhmlmod1 G S LMHom T S LMod
15 14 3ad2ant1 G S LMHom T G : B 1-1 C F B S LMod
16 1 islinds S LMod F LIndS S F B I F LIndF S
17 15 16 syl G S LMHom T G : B 1-1 C F B F LIndS S F B I F LIndF S
18 lmhmlmod2 G S LMHom T T LMod
19 18 3ad2ant1 G S LMHom T G : B 1-1 C F B T LMod
20 19 adantr G S LMHom T G : B 1-1 C F B G F LIndS T T LMod
21 simpr G S LMHom T G : B 1-1 C F B G F LIndS T G F LIndS T
22 f1ores G : B 1-1 C F 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 B G F : F 1-1 G F
25 24 3adant1 G S LMHom T G : B 1-1 C F B G F : F 1-1 G F
26 25 adantr G S LMHom T G : B 1-1 C F B G F LIndS T G F : F 1-1 G F
27 f1linds T LMod G F LIndS T G F : F 1-1 G F G F LIndF T
28 20 21 26 27 syl3anc G S LMHom T G : B 1-1 C F B G F LIndS T G F LIndF T
29 df-ima G F = ran G F
30 lindfrn T LMod G F LIndF T ran G F LIndS T
31 19 30 sylan G S LMHom T G : B 1-1 C F B G F LIndF T ran G F LIndS T
32 29 31 eqeltrid G S LMHom T G : B 1-1 C F B G F LIndF T G F LIndS T
33 28 32 impbida G S LMHom T G : B 1-1 C F B G F LIndS T G F LIndF T
34 coires1 G I F = G F
35 34 breq1i G I F LIndF T G F LIndF T
36 33 35 bitr4di G S LMHom T G : B 1-1 C F B G F LIndS T G I F LIndF T
37 13 17 36 3bitr4d G S LMHom T G : B 1-1 C F B F LIndS S G F LIndS T