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