Theorem islindf5

Description: A family is independent iff the linear combinations homomorphism is injective. (Contributed by Stefan O'Rear, 28-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		islindf5.f	$$⊢F=R\mathrm{freeLMod}I$$
2		islindf5.b	$$⊢B={\mathrm{Base}}_F$$
3		islindf5.c	$$⊢C={\mathrm{Base}}_T$$
4		islindf5.v	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
5		islindf5.e	$$⊢E=\left(x\in B⟼{\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)\right)$$
6		islindf5.t	$$⊢\phi \to T\in \mathrm{LMod}$$
7		islindf5.i	$$⊢\phi \to I\in X$$
8		islindf5.r	$$⊢\phi \to R=\mathrm{Scalar}\left(T\right)$$
9		islindf5.a	$$⊢\phi \to A:I⟶C$$
10		eqid	$$⊢\mathrm{Scalar}\left(T\right)=\mathrm{Scalar}\left(T\right)$$
11		eqid	$$⊢0_T=0_T$$
12		eqid	$$⊢0_{\mathrm{Scalar}\left(T\right)}=0_{\mathrm{Scalar}\left(T\right)}$$
13		eqid	$$⊢{\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}={\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}$$
14	3 10 4 11 12 13	islindf4	$$⊢\left(T\in \mathrm{LMod}\wedge I\in X\wedge A:I⟶C\right)\to \left(A\mathrm{LIndF}T\leftrightarrow \forall y\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}\left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\right)$$
15	6 7 9 14	syl3anc	$$⊢\phi \to \left(A\mathrm{LIndF}T\leftrightarrow \forall y\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}\left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\right)$$
16		oveq1	$$⊢x=y\to x{\underset{\dot{}}{·}}_{f}A=y{\underset{\dot{}}{·}}_{f}A$$
17	16	oveq2d	$$⊢x=y\to {\sum }_T\left(x{\underset{\dot{}}{·}}_{f}A\right)={\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)$$
18		ovex	$$⊢{\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)\in \mathrm{V}$$
19	17 5 18	fvmpt	$$⊢y\in B\to E\left(y\right)={\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)$$
20	19	adantl	$$⊢\left(\phi \wedge y\in B\right)\to E\left(y\right)={\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)$$
21	20	eqeq1d	$$⊢\left(\phi \wedge y\in B\right)\to \left(E\left(y\right)=0_T\leftrightarrow {\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\right)$$
22	10	lmodring	$$⊢T\in \mathrm{LMod}\to \mathrm{Scalar}\left(T\right)\in \mathrm{Ring}$$
23	6 22	syl	$$⊢\phi \to \mathrm{Scalar}\left(T\right)\in \mathrm{Ring}$$
24	8 23	eqeltrd	$$⊢\phi \to R\in \mathrm{Ring}$$
25		eqid	$$⊢0_R=0_R$$
26	1 25	frlm0	$$⊢\left(R\in \mathrm{Ring}\wedge I\in X\right)\to I\times \left\{0_R\right\}=0_F$$
27	24 7 26	syl2anc	$$⊢\phi \to I\times \left\{0_R\right\}=0_F$$
28	8	fveq2d	$$⊢\phi \to 0_R=0_{\mathrm{Scalar}\left(T\right)}$$
29	28	sneqd	$$⊢\phi \to \left\{0_R\right\}=\left\{0_{\mathrm{Scalar}\left(T\right)}\right\}$$
30	29	xpeq2d	$$⊢\phi \to I\times \left\{0_R\right\}=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}$$
31	27 30	eqtr3d	$$⊢\phi \to 0_F=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}$$
32	31	adantr	$$⊢\left(\phi \wedge y\in B\right)\to 0_F=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}$$
33	32	eqeq2d	$$⊢\left(\phi \wedge y\in B\right)\to \left(y=0_F\leftrightarrow y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)$$
34	21 33	imbi12d	$$⊢\left(\phi \wedge y\in B\right)\to \left(\left(E\left(y\right)=0_T\to y=0_F\right)\leftrightarrow \left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\right)$$
35	34	ralbidva	$$⊢\phi \to \left(\forall y\in B\left(E\left(y\right)=0_T\to y=0_F\right)\leftrightarrow \forall y\in B\left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\right)$$
36	8	eqcomd	$$⊢\phi \to \mathrm{Scalar}\left(T\right)=R$$
37	36	oveq1d	$$⊢\phi \to \mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I=R\mathrm{freeLMod}I$$
38	37 1	eqtr4di	$$⊢\phi \to \mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I=F$$
39	38	fveq2d	$$⊢\phi \to {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}={\mathrm{Base}}_F$$
40	39 2	eqtr4di	$$⊢\phi \to {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}=B$$
41	40	raleqdv	$$⊢\phi \to \left(\forall y\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}\left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\leftrightarrow \forall y\in B\left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\right)$$
42	35 41	bitr4d	$$⊢\phi \to \left(\forall y\in B\left(E\left(y\right)=0_T\to y=0_F\right)\leftrightarrow \forall y\in {\mathrm{Base}}_{\left(\mathrm{Scalar}\left(T\right)\mathrm{freeLMod}I\right)}\left({\sum }_T\left(y{\underset{\dot{}}{·}}_{f}A\right)=0_T\to y=I\times \left\{0_{\mathrm{Scalar}\left(T\right)}\right\}\right)\right)$$
43	15 42	bitr4d	$$⊢\phi \to \left(A\mathrm{LIndF}T\leftrightarrow \forall y\in B\left(E\left(y\right)=0_T\to y=0_F\right)\right)$$
44	1 2 3 4 5 6 7 8 9	frlmup1	$$⊢\phi \to E\in \left(F\mathrm{LMHom}T\right)$$
45		lmghm	$$⊢E\in \left(F\mathrm{LMHom}T\right)\to E\in \left(F\mathrm{GrpHom}T\right)$$
46		eqid	$$⊢0_F=0_F$$
47	2 3 46 11	ghmf1	$$⊢E\in \left(F\mathrm{GrpHom}T\right)\to \left(E:B\underset{1-1}{⟶}C\leftrightarrow \forall y\in B\left(E\left(y\right)=0_T\to y=0_F\right)\right)$$
48	44 45 47	3syl	$$⊢\phi \to \left(E:B\underset{1-1}{⟶}C\leftrightarrow \forall y\in B\left(E\left(y\right)=0_T\to y=0_F\right)\right)$$
49	43 48	bitr4d	$$⊢\phi \to \left(A\mathrm{LIndF}T\leftrightarrow E:B\underset{1-1}{⟶}C\right)$$