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