Theorem indlcim

Description: An independent, spanning family extends to an isomorphism from a free module. (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Hypotheses	indlcim.f	$$⊢F=R\mathrm{freeLMod}I$$
	indlcim.b	$$⊢B={\mathrm{Base}}_F$$
	indlcim.c	$$⊢C={\mathrm{Base}}_T$$
	indlcim.v	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
	indlcim.n	$$⊢N=\mathrm{LSpan}\left(T\right)$$
	indlcim.e	$$⊢E=\left(x\in B⟼{\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)\right)$$
	indlcim.t	$$⊢\phi \to T\in \mathrm{LMod}$$
	indlcim.i	$$⊢\phi \to I\in X$$
	indlcim.r	$$⊢\phi \to R=\mathrm{Scalar}\left(T\right)$$
	indlcim.a	$$⊢\phi \to A:I\underset{onto}{⟶}J$$
	indlcim.l	$$⊢\phi \to A\mathrm{LIndF}T$$
	indlcim.s	$$⊢\phi \to N\left(J\right)=C$$
Assertion	indlcim	$$⊢\phi \to E\in \left(F\mathrm{LMIso}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		indlcim.f	$$⊢F=R\mathrm{freeLMod}I$$
2		indlcim.b	$$⊢B={\mathrm{Base}}_F$$
3		indlcim.c	$$⊢C={\mathrm{Base}}_T$$
4		indlcim.v	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
5		indlcim.n	$$⊢N=\mathrm{LSpan}\left(T\right)$$
6		indlcim.e	$$⊢E=\left(x\in B⟼{\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)\right)$$
7		indlcim.t	$$⊢\phi \to T\in \mathrm{LMod}$$
8		indlcim.i	$$⊢\phi \to I\in X$$
9		indlcim.r	$$⊢\phi \to R=\mathrm{Scalar}\left(T\right)$$
10		indlcim.a	$$⊢\phi \to A:I\underset{onto}{⟶}J$$
11		indlcim.l	$$⊢\phi \to A\mathrm{LIndF}T$$
12		indlcim.s	$$⊢\phi \to N\left(J\right)=C$$
13		fofn	$$⊢A:I\underset{onto}{⟶}J\to AFnI$$
14	10 13	syl	$$⊢\phi \to AFnI$$
15	3	lindff	$$⊢\left(A\mathrm{LIndF}T\wedge T\in \mathrm{LMod}\right)\to A:\mathrm{dom}A⟶C$$
16	11 7 15	syl2anc	$$⊢\phi \to A:\mathrm{dom}A⟶C$$
17	16	frnd	$$⊢\phi \to \mathrm{ran}A\subseteq C$$
18		df-f	$$⊢A:I⟶C\leftrightarrow \left(AFnI\wedge \mathrm{ran}A\subseteq C\right)$$
19	14 17 18	sylanbrc	$$⊢\phi \to A:I⟶C$$
20	1 2 3 4 6 7 8 9 19	frlmup1	$$⊢\phi \to E\in \left(F\mathrm{LMHom}T\right)$$
21	1 2 3 4 6 7 8 9 19	islindf5	$$⊢\phi \to \left(A\mathrm{LIndF}T\leftrightarrow E:B\underset{1-1}{⟶}C\right)$$
22	11 21	mpbid	$$⊢\phi \to E:B\underset{1-1}{⟶}C$$
23	1 2 3 4 6 7 8 9 19 5	frlmup3	$$⊢\phi \to \mathrm{ran}E=N\left(\mathrm{ran}A\right)$$
24		forn	$$⊢A:I\underset{onto}{⟶}J\to \mathrm{ran}A=J$$
25	10 24	syl	$$⊢\phi \to \mathrm{ran}A=J$$
26	25	fveq2d	$$⊢\phi \to N\left(\mathrm{ran}A\right)=N\left(J\right)$$
27	23 26 12	3eqtrd	$$⊢\phi \to \mathrm{ran}E=C$$
28		dff1o5	$$⊢E:B\underset{1-1\; onto}{⟶}C\leftrightarrow \left(E:B\underset{1-1}{⟶}C\wedge \mathrm{ran}E=C\right)$$
29	22 27 28	sylanbrc	$$⊢\phi \to E:B\underset{1-1\; onto}{⟶}C$$
30	2 3	islmim	$$⊢E\in \left(F\mathrm{LMIso}T\right)\leftrightarrow \left(E\in \left(F\mathrm{LMHom}T\right)\wedge E:B\underset{1-1\; onto}{⟶}C\right)$$
31	20 29 30	sylanbrc	$$⊢\phi \to E\in \left(F\mathrm{LMIso}T\right)$$