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	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to F LIndF W$

Step	Hyp	Ref	Expression
1		f1f	$⊢ F : D \underset{1-1}{⟶} S \to F : D ⟶ S$
2		fcoi2	$⊢ F : D ⟶ S \to ({I ↾}_{S}) \circ F = F$
3	1 2	syl	$⊢ F : D \underset{1-1}{⟶} S \to ({I ↾}_{S}) \circ F = F$
4	3	3ad2ant3	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to ({I ↾}_{S}) \circ F = F$
5		simp1	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to W \in LMod$
6		linds2	$⊢ S \in LIndS (W) \to ({I ↾}_{S}) LIndF W$
7	6	3ad2ant2	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to ({I ↾}_{S}) LIndF W$
8		dmresi	$⊢ dom ({I ↾}_{S}) = S$
9		f1eq3	$⊢ dom ({I ↾}_{S}) = S \to (F : D \underset{1-1}{⟶} dom ({I ↾}_{S}) \leftrightarrow F : D \underset{1-1}{⟶} S)$
10	8 9	ax-mp	$⊢ F : D \underset{1-1}{⟶} dom ({I ↾}_{S}) \leftrightarrow F : D \underset{1-1}{⟶} S$
11	10	biimpri	$⊢ F : D \underset{1-1}{⟶} S \to F : D \underset{1-1}{⟶} dom ({I ↾}_{S})$
12	11	3ad2ant3	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to F : D \underset{1-1}{⟶} dom ({I ↾}_{S})$
13		f1lindf	$⊢ (W \in LMod \land ({I ↾}_{S}) LIndF W \land F : D \underset{1-1}{⟶} dom ({I ↾}_{S})) \to (({I ↾}_{S}) \circ F) LIndF W$
14	5 7 12 13	syl3anc	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to (({I ↾}_{S}) \circ F) LIndF W$
15	4 14	eqbrtrrd	$⊢ (W \in LMod \land S \in LIndS (W) \land F : D \underset{1-1}{⟶} S) \to F LIndF W$

Metamath Proof Explorer