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 \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F \in LIndS (S)) \to G [F] \in LIndS (T)$

Step	Hyp	Ref	Expression
1		lindfmm.b	$⊢ B = {Base}_{S}$
2		lindfmm.c	$⊢ C = {Base}_{T}$
3		simp3	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F \in LIndS (S)) \to F \in LIndS (S)$
4	1	linds1	$⊢ F \in LIndS (S) \to F \subseteq B$
5	1 2	lindsmm	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F \subseteq B) \to (F \in LIndS (S) \leftrightarrow G [F] \in LIndS (T))$
6	4 5	syl3an3	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F \in LIndS (S)) \to (F \in LIndS (S) \leftrightarrow G [F] \in LIndS (T))$
7	3 6	mpbid	$⊢ (G \in (S LMHom T) \land G : B \underset{1-1}{⟶} C \land F \in LIndS (S)) \to G [F] \in LIndS (T)$

Metamath Proof Explorer