Metamath Proof Explorer

Theorem lindsmm2

Description: The monomorphic image of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lindfmm.b ⊢ B = Base S
lindfmm.c ⊢ C = Base T
Assertion lindsmm2 ⊢ G ∈ S LMHom T ∧ G : B ⟶ 1-1 C ∧ 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 simp3 ⊢ G ∈ S LMHom T ∧ G : B ⟶ 1-1 C ∧ F ∈ LIndS ⁡ S → F ∈ LIndS ⁡ S
4 1 linds1 ⊢ F ∈ LIndS ⁡ S → F ⊆ B
5 1 2 lindsmm ⊢ G ∈ S LMHom T ∧ G : B ⟶ 1-1 C ∧ F ⊆ B → F ∈ LIndS ⁡ S ↔ G F ∈ LIndS ⁡ T
6 4 5 syl3an3 ⊢ G ∈ S LMHom T ∧ G : B ⟶ 1-1 C ∧ F ∈ LIndS ⁡ S → F ∈ LIndS ⁡ S ↔ G F ∈ LIndS ⁡ T
7 3 6 mpbid ⊢ G ∈ S LMHom T ∧ G : B ⟶ 1-1 C ∧ F ∈ LIndS ⁡ S → G F ∈ LIndS ⁡ T