Theorem asclghm

Description: The algebra scalar lifting function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	asclf.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclf.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	asclf.r	$$⊢\phi \to W\in \mathrm{Ring}$$
	asclf.l	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	asclghm	$$⊢\phi \to A\in \left(F\mathrm{GrpHom}W\right)$$

Proof

Step	Hyp	Ref	Expression
1		asclf.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclf.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		asclf.r	$$⊢\phi \to W\in \mathrm{Ring}$$
4		asclf.l	$$⊢\phi \to W\in \mathrm{LMod}$$
5		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
6		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
7		eqid	$$⊢{+}_F={+}_F$$
8		eqid	$$⊢{+}_W={+}_W$$
9	2	lmodring	$$⊢W\in \mathrm{LMod}\to F\in \mathrm{Ring}$$
10	4 9	syl	$$⊢\phi \to F\in \mathrm{Ring}$$
11		ringgrp	$$⊢F\in \mathrm{Ring}\to F\in \mathrm{Grp}$$
12	10 11	syl	$$⊢\phi \to F\in \mathrm{Grp}$$
13		ringgrp	$$⊢W\in \mathrm{Ring}\to W\in \mathrm{Grp}$$
14	3 13	syl	$$⊢\phi \to W\in \mathrm{Grp}$$
15	1 2 3 4 5 6	asclf	$$⊢\phi \to A:{\mathrm{Base}}_F⟶{\mathrm{Base}}_W$$
16	4	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to W\in \mathrm{LMod}$$
17		simprl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to x\in {\mathrm{Base}}_F$$
18		simprr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to y\in {\mathrm{Base}}_F$$
19		eqid	$$⊢1_W=1_W$$
20	6 19	ringidcl	$$⊢W\in \mathrm{Ring}\to 1_W\in {\mathrm{Base}}_W$$
21	3 20	syl	$$⊢\phi \to 1_W\in {\mathrm{Base}}_W$$
22	21	adantr	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to 1_W\in {\mathrm{Base}}_W$$
23		eqid	$$⊢{\cdot }_W={\cdot }_W$$
24	6 8 2 23 5 7	lmodvsdir	$$⊢\left(W\in \mathrm{LMod}\wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\wedge 1_W\in {\mathrm{Base}}_W\right)\right)\to \left(x{+}_{F}y\right){\cdot }_W{1}_W=\left(x{\cdot }_W{1}_W\right){+}_W\left(y{\cdot }_W{1}_W\right)$$
25	16 17 18 22 24	syl13anc	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to \left(x{+}_{F}y\right){\cdot }_W{1}_W=\left(x{\cdot }_W{1}_W\right){+}_W\left(y{\cdot }_W{1}_W\right)$$
26	5 7	grpcl	$$⊢\left(F\in \mathrm{Grp}\wedge x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\to x{+}_{F}y\in {\mathrm{Base}}_F$$
27	26	3expb	$$⊢\left(F\in \mathrm{Grp}\wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to x{+}_{F}y\in {\mathrm{Base}}_F$$
28	12 27	sylan	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to x{+}_{F}y\in {\mathrm{Base}}_F$$
29	1 2 5 23 19	asclval	$$⊢x{+}_{F}y\in {\mathrm{Base}}_F\to A\left(x{+}_{F}y\right)=\left(x{+}_{F}y\right){\cdot }_W{1}_W$$
30	28 29	syl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to A\left(x{+}_{F}y\right)=\left(x{+}_{F}y\right){\cdot }_W{1}_W$$
31	1 2 5 23 19	asclval	$$⊢x\in {\mathrm{Base}}_F\to A\left(x\right)=x{\cdot }_W{1}_W$$
32	1 2 5 23 19	asclval	$$⊢y\in {\mathrm{Base}}_F\to A\left(y\right)=y{\cdot }_W{1}_W$$
33	31 32	oveqan12d	$$⊢\left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\to A\left(x\right){+}_{W}A\left(y\right)=\left(x{\cdot }_W{1}_W\right){+}_W\left(y{\cdot }_W{1}_W\right)$$
34	33	adantl	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to A\left(x\right){+}_{W}A\left(y\right)=\left(x{\cdot }_W{1}_W\right){+}_W\left(y{\cdot }_W{1}_W\right)$$
35	25 30 34	3eqtr4d	$$⊢\left(\phi \wedge \left(x\in {\mathrm{Base}}_F\wedge y\in {\mathrm{Base}}_F\right)\right)\to A\left(x{+}_{F}y\right)=A\left(x\right){+}_{W}A\left(y\right)$$
36	5 6 7 8 12 14 15 35	isghmd	$$⊢\phi \to A\in \left(F\mathrm{GrpHom}W\right)$$