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 ) )