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