Theorem lindfres

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

	Ref	Expression
Assertion	lindfres	$$⊢\left(W\in \mathrm{LMod}\wedge F\mathrm{LIndF}W\right)\to \left({F\upharpoonright }_X\right)\mathrm{LIndF}W$$

Proof

Step	Hyp	Ref	Expression
1		coires1	$$⊢F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right)={F\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}$$
2		resdmres	$$⊢{F\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}={F\upharpoonright }_X$$
3	1 2	eqtri	$$⊢F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right)={F\upharpoonright }_X$$
4		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({F\upharpoonright }_X\right)$$
5		f1of1	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\left({F\upharpoonright }_X\right)\to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1}{⟶}\mathrm{dom}\left({F\upharpoonright }_X\right)$$
6	4 5	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1}{⟶}\mathrm{dom}\left({F\upharpoonright }_X\right)$$
7		resss	$$⊢{F\upharpoonright }_X\subseteq F$$
8		dmss	$$⊢{F\upharpoonright }_X\subseteq F\to \mathrm{dom}\left({F\upharpoonright }_X\right)\subseteq \mathrm{dom}F$$
9	7 8	ax-mp	$$⊢\mathrm{dom}\left({F\upharpoonright }_X\right)\subseteq \mathrm{dom}F$$
10		f1ss	$$⊢\left(\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1}{⟶}\mathrm{dom}\left({F\upharpoonright }_X\right)\wedge \mathrm{dom}\left({F\upharpoonright }_X\right)\subseteq \mathrm{dom}F\right)\to \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1}{⟶}\mathrm{dom}F$$
11	6 9 10	mp2an	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1}{⟶}\mathrm{dom}F$$
12		f1lindf	$$⊢\left(W\in \mathrm{LMod}\wedge F\mathrm{LIndF}W\wedge \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right):\mathrm{dom}\left({F\upharpoonright }_X\right)\underset{1-1}{⟶}\mathrm{dom}F\right)\to \left(F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right)\right)\mathrm{LIndF}W$$
13	11 12	mp3an3	$$⊢\left(W\in \mathrm{LMod}\wedge F\mathrm{LIndF}W\right)\to \left(F\circ \left({\mathrm{I}\upharpoonright }_{\mathrm{dom}\left({F\upharpoonright }_X\right)}\right)\right)\mathrm{LIndF}W$$
14	3 13	eqbrtrrid	$$⊢\left(W\in \mathrm{LMod}\wedge F\mathrm{LIndF}W\right)\to \left({F\upharpoonright }_X\right)\mathrm{LIndF}W$$