Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  asclghm Structured version   Unicode version

Theorem asclghm 16397
 Description: The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.)
Hypotheses
Ref Expression
asclf.a algSc
asclf.f Scalar
asclf.r
asclf.l
Assertion
Ref Expression
asclghm

Proof of Theorem asclghm
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2436 . 2
2 eqid 2436 . 2
3 eqid 2436 . 2
4 eqid 2436 . 2
5 asclf.l . . . 4
6 asclf.f . . . . 5 Scalar
76lmodrng 15958 . . . 4
85, 7syl 16 . . 3
9 rnggrp 15669 . . 3
108, 9syl 16 . 2
11 asclf.r . . 3
12 rnggrp 15669 . . 3
1311, 12syl 16 . 2
14 asclf.a . . 3 algSc
1514, 6, 11, 5, 1, 2asclf 16396 . 2
165adantr 452 . . . 4
17 simprl 733 . . . 4
18 simprr 734 . . . 4
19 eqid 2436 . . . . . . 7
202, 19rngidcl 15684 . . . . . 6
2111, 20syl 16 . . . . 5
2221adantr 452 . . . 4
23 eqid 2436 . . . . 5
242, 4, 6, 23, 1, 3lmodvsdir 15974 . . . 4
2516, 17, 18, 22, 24syl13anc 1186 . . 3
261, 3grpcl 14818 . . . . . 6
27263expb 1154 . . . . 5
2810, 27sylan 458 . . . 4
2914, 6, 1, 23, 19asclval 16394 . . . 4
3028, 29syl 16 . . 3
3114, 6, 1, 23, 19asclval 16394 . . . . 5
3214, 6, 1, 23, 19asclval 16394 . . . . 5
3331, 32oveqan12d 6100 . . . 4