This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ( S LMHom T ) /\ G : B -1-1-> C /\ 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 simp3 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F e. ( LIndS ` S ) ) -> F e. ( LIndS ` S ) )
4 1 linds1 
 |-  ( F e. ( LIndS ` S ) -> F C_ B )
5 1 2 lindsmm 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F C_ B ) -> ( F e. ( LIndS ` S ) <-> ( G " F ) e. ( LIndS ` T ) ) )
6 4 5 syl3an3 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F e. ( LIndS ` S ) ) -> ( F e. ( LIndS ` S ) <-> ( G " F ) e. ( LIndS ` T ) ) )
7 3 6 mpbid 
 |-  ( ( G e. ( S LMHom T ) /\ G : B -1-1-> C /\ F e. ( LIndS ` S ) ) -> ( G " F ) e. ( LIndS ` T ) )