# Metamath Proof Explorer

## Theorem asclghm

Description: The algebra scalars 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)$