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

Metamath Proof Explorer

Theorem f1linds

Description: A family constructed from non-repeated elements of an independent set is independent. (Contributed by Stefan O'Rear, 26-Feb-2015)

Ref Expression
Assertion f1linds ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝐹 LIndF 𝑊 )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : 𝐷 –1-1→ 𝑆 → 𝐹 : 𝐷 ⟶ 𝑆 )
2 fcoi2 ⊢ ( 𝐹 : 𝐷 ⟶ 𝑆 → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) = 𝐹 )
3 1 2 syl ⊢ ( 𝐹 : 𝐷 –1-1→ 𝑆 → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) = 𝐹 )
4 3 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) = 𝐹 )
5 simp1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝑊 ∈ LMod )
6 linds2 ⊢ ( 𝑆 ∈ ( LIndS ‘ 𝑊 ) → ( I ↾ 𝑆 ) LIndF 𝑊 )
7 6 3ad2ant2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → ( I ↾ 𝑆 ) LIndF 𝑊 )
8 dmresi ⊢ dom ( I ↾ 𝑆 ) = 𝑆
9 f1eq3 ⊢ ( dom ( I ↾ 𝑆 ) = 𝑆 → ( 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ↔ 𝐹 : 𝐷 –1-1→ 𝑆 ) )
10 8 9 ax-mp ⊢ ( 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ↔ 𝐹 : 𝐷 –1-1→ 𝑆 )
11 10 biimpri ⊢ ( 𝐹 : 𝐷 –1-1→ 𝑆 → 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) )
12 11 3ad2ant3 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) )
13 f1lindf ⊢ ( ( 𝑊 ∈ LMod ∧ ( I ↾ 𝑆 ) LIndF 𝑊 ∧ 𝐹 : 𝐷 –1-1→ dom ( I ↾ 𝑆 ) ) → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) LIndF 𝑊 )
14 5 7 12 13 syl3anc ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → ( ( I ↾ 𝑆 ) ∘ 𝐹 ) LIndF 𝑊 )
15 4 14 eqbrtrrd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑆 ∈ ( LIndS ‘ 𝑊 ) ∧ 𝐹 : 𝐷 –1-1→ 𝑆 ) → 𝐹 LIndF 𝑊 )