Theorem lindfres

Description: Any restriction of an independent family is independent. (Contributed by Stefan O'Rear, 24-Feb-2015)

	Ref	Expression
Assertion	lindfres	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 ↾ 𝑋 ) LIndF 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		coires1	⊢ ( 𝐹 ∘ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) ) = ( 𝐹 ↾ dom ( 𝐹 ↾ 𝑋 ) )
2		resdmres	⊢ ( 𝐹 ↾ dom ( 𝐹 ↾ 𝑋 ) ) = ( 𝐹 ↾ 𝑋 )
3	1 2	eqtri	⊢ ( 𝐹 ∘ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) ) = ( 𝐹 ↾ 𝑋 )
4		f1oi	⊢ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1-onto→ dom ( 𝐹 ↾ 𝑋 )
5		f1of1	⊢ ( ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1-onto→ dom ( 𝐹 ↾ 𝑋 ) → ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1→ dom ( 𝐹 ↾ 𝑋 ) )
6	4 5	ax-mp	⊢ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1→ dom ( 𝐹 ↾ 𝑋 )
7		resss	⊢ ( 𝐹 ↾ 𝑋 ) ⊆ 𝐹
8		dmss	⊢ ( ( 𝐹 ↾ 𝑋 ) ⊆ 𝐹 → dom ( 𝐹 ↾ 𝑋 ) ⊆ dom 𝐹 )
9	7 8	ax-mp	⊢ dom ( 𝐹 ↾ 𝑋 ) ⊆ dom 𝐹
10		f1ss	⊢ ( ( ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1→ dom ( 𝐹 ↾ 𝑋 ) ∧ dom ( 𝐹 ↾ 𝑋 ) ⊆ dom 𝐹 ) → ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1→ dom 𝐹 )
11	6 9 10	mp2an	⊢ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1→ dom 𝐹
12		f1lindf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ∧ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) : dom ( 𝐹 ↾ 𝑋 ) –1-1→ dom 𝐹 ) → ( 𝐹 ∘ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) ) LIndF 𝑊 )
13	11 12	mp3an3	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 ∘ ( I ↾ dom ( 𝐹 ↾ 𝑋 ) ) ) LIndF 𝑊 )
14	3 13	eqbrtrrid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 LIndF 𝑊 ) → ( 𝐹 ↾ 𝑋 ) LIndF 𝑊 )