Metamath Proof Explorer


Theorem asclrhm

Description: The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015)

Ref Expression
Hypotheses asclrhm.a A = algSc W
asclrhm.f F = Scalar W
Assertion asclrhm W AssAlg A F RingHom W

Proof

Step Hyp Ref Expression
1 asclrhm.a A = algSc W
2 asclrhm.f F = Scalar W
3 eqid Base F = Base F
4 eqid 1 F = 1 F
5 eqid 1 W = 1 W
6 eqid F = F
7 eqid W = W
8 2 assasca W AssAlg F CRing
9 crngring F CRing F Ring
10 8 9 syl W AssAlg F Ring
11 assaring W AssAlg W Ring
12 3 4 ringidcl F Ring 1 F Base F
13 eqid W = W
14 1 2 3 13 5 asclval 1 F Base F A 1 F = 1 F W 1 W
15 10 12 14 3syl W AssAlg A 1 F = 1 F W 1 W
16 assalmod W AssAlg W LMod
17 eqid Base W = Base W
18 17 5 ringidcl W Ring 1 W Base W
19 11 18 syl W AssAlg 1 W Base W
20 17 2 13 4 lmodvs1 W LMod 1 W Base W 1 F W 1 W = 1 W
21 16 19 20 syl2anc W AssAlg 1 F W 1 W = 1 W
22 15 21 eqtrd W AssAlg A 1 F = 1 W
23 1 2 3 7 6 ascldimul W AssAlg x Base F y Base F A x F y = A x W A y
24 23 3expb W AssAlg x Base F y Base F A x F y = A x W A y
25 1 2 11 16 asclghm W AssAlg A F GrpHom W
26 3 4 5 6 7 10 11 22 24 25 isrhm2d W AssAlg A F RingHom W