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

Metamath Proof Explorer

Theorem lindsmm

Description: Linear independence of a set is unchanged by injective linear functions. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Hypotheses lindfmm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
lindfmm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
Assertion lindsmm ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) ↔ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 lindfmm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
2 lindfmm.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 ibar ⊢ ( 𝐹 ⊆ 𝐵 → ( ( I ↾ 𝐹 ) LIndF 𝑆 ↔ ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑆 ) ) )
4 3 3ad2ant3 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( ( I ↾ 𝐹 ) LIndF 𝑆 ↔ ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑆 ) ) )
5 f1oi ⊢ ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹
6 f1of ⊢ ( ( I ↾ 𝐹 ) : 𝐹 –1-1-onto→ 𝐹 → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 )
7 5 6 ax-mp ⊢ ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹
8 simp3 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → 𝐹 ⊆ 𝐵 )
9 fss ⊢ ( ( ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐹 ∧ 𝐹 ⊆ 𝐵 ) → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
10 7 8 9 sylancr ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
11 1 2 lindfmm ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ ( I ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 ) → ( ( I ↾ 𝐹 ) LIndF 𝑆 ↔ ( 𝐺 ∘ ( I ↾ 𝐹 ) ) LIndF 𝑇 ) )
12 10 11 syld3an3 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( ( I ↾ 𝐹 ) LIndF 𝑆 ↔ ( 𝐺 ∘ ( I ↾ 𝐹 ) ) LIndF 𝑇 ) )
13 4 12 bitr3d ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑆 ) ↔ ( 𝐺 ∘ ( I ↾ 𝐹 ) ) LIndF 𝑇 ) )
14 lmhmlmod1 ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
15 14 3ad2ant1 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → 𝑆 ∈ LMod )
16 1 islinds ⊢ ( 𝑆 ∈ LMod → ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑆 ) ) )
17 15 16 syl ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) ↔ ( 𝐹 ⊆ 𝐵 ∧ ( I ↾ 𝐹 ) LIndF 𝑆 ) ) )
18 lmhmlmod2 ⊢ ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑇 ∈ LMod )
19 18 3ad2ant1 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → 𝑇 ∈ LMod )
20 19 adantr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) ∧ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) → 𝑇 ∈ LMod )
21 simpr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) ∧ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) → ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) )
22 f1ores ⊢ ( ( 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1-onto→ ( 𝐺 “ 𝐹 ) )
23 f1of1 ⊢ ( ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1-onto→ ( 𝐺 “ 𝐹 ) → ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1→ ( 𝐺 “ 𝐹 ) )
24 22 23 syl ⊢ ( ( 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1→ ( 𝐺 “ 𝐹 ) )
25 24 3adant1 ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1→ ( 𝐺 “ 𝐹 ) )
26 25 adantr ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) ∧ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) → ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1→ ( 𝐺 “ 𝐹 ) )
27 f1linds ⊢ ( ( 𝑇 ∈ LMod ∧ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ∧ ( 𝐺 ↾ 𝐹 ) : 𝐹 –1-1→ ( 𝐺 “ 𝐹 ) ) → ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 )
28 20 21 26 27 syl3anc ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) ∧ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) → ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 )
29 df-ima ⊢ ( 𝐺 “ 𝐹 ) = ran ( 𝐺 ↾ 𝐹 )
30 lindfrn ⊢ ( ( 𝑇 ∈ LMod ∧ ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 ) → ran ( 𝐺 ↾ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) )
31 19 30 sylan ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) ∧ ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 ) → ran ( 𝐺 ↾ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) )
32 29 31 eqeltrid ⊢ ( ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) ∧ ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 ) → ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) )
33 28 32 impbida ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ↔ ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 ) )
34 coires1 ⊢ ( 𝐺 ∘ ( I ↾ 𝐹 ) ) = ( 𝐺 ↾ 𝐹 )
35 34 breq1i ⊢ ( ( 𝐺 ∘ ( I ↾ 𝐹 ) ) LIndF 𝑇 ↔ ( 𝐺 ↾ 𝐹 ) LIndF 𝑇 )
36 33 35 bitr4di ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ↔ ( 𝐺 ∘ ( I ↾ 𝐹 ) ) LIndF 𝑇 ) )
37 13 17 36 3bitr4d ⊢ ( ( 𝐺 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐺 : 𝐵 –1-1→ 𝐶 ∧ 𝐹 ⊆ 𝐵 ) → ( 𝐹 ∈ ( LIndS ‘ 𝑆 ) ↔ ( 𝐺 “ 𝐹 ) ∈ ( LIndS ‘ 𝑇 ) ) )