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 ⊢ 𝐵 = ( Base ‘ 𝑆 )
lindfmm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
Assertion lindsmm2 ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ∈ ( LIndS ‘ 𝑆 ) ) → ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 lindfmm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 lindfmm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 simp3 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ∈ ( LIndS ‘ 𝑆 ) ) → 𝐹 ∈ ( LIndS ‘ 𝑆 ) )
4 1 linds1 ⊢ ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) → 𝐹 ⊆ 𝐵 )
5 1 2 lindsmm ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) ↔ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) )
6 4 5 syl3an3 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ∈ ( LIndS ‘ 𝑆 ) ) → ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) ↔ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) )
7 3 6 mpbid ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ∈ ( LIndS ‘ 𝑆 ) ) → ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) )