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 ⊢ W ∈ LMod ∧ F LIndF W → F ↾ X LIndF W

Proof

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