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

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