Metamath Proof Explorer


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