Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’
(BaseβπΉ) =
(BaseβπΉ) |
2 | | eqid 2733 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2733 |
. 2
β’
(+gβπΉ) = (+gβπΉ) |
4 | | eqid 2733 |
. 2
β’
(+gβπ) = (+gβπ) |
5 | | asclf.l |
. . . 4
β’ (π β π β LMod) |
6 | | asclf.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
7 | 6 | lmodring 20344 |
. . . 4
β’ (π β LMod β πΉ β Ring) |
8 | 5, 7 | syl 17 |
. . 3
β’ (π β πΉ β Ring) |
9 | | ringgrp 19974 |
. . 3
β’ (πΉ β Ring β πΉ β Grp) |
10 | 8, 9 | syl 17 |
. 2
β’ (π β πΉ β Grp) |
11 | | asclf.r |
. . 3
β’ (π β π β Ring) |
12 | | ringgrp 19974 |
. . 3
β’ (π β Ring β π β Grp) |
13 | 11, 12 | syl 17 |
. 2
β’ (π β π β Grp) |
14 | | asclf.a |
. . 3
β’ π΄ = (algScβπ) |
15 | 14, 6, 11, 5, 1, 2 | asclf 21301 |
. 2
β’ (π β π΄:(BaseβπΉ)βΆ(Baseβπ)) |
16 | 5 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β π β LMod) |
17 | | simprl 770 |
. . . 4
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β π₯ β (BaseβπΉ)) |
18 | | simprr 772 |
. . . 4
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β π¦ β (BaseβπΉ)) |
19 | | eqid 2733 |
. . . . . . 7
β’
(1rβπ) = (1rβπ) |
20 | 2, 19 | ringidcl 19994 |
. . . . . 6
β’ (π β Ring β
(1rβπ)
β (Baseβπ)) |
21 | 11, 20 | syl 17 |
. . . . 5
β’ (π β (1rβπ) β (Baseβπ)) |
22 | 21 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β (1rβπ) β (Baseβπ)) |
23 | | eqid 2733 |
. . . . 5
β’ (
Β·π βπ) = ( Β·π
βπ) |
24 | 2, 4, 6, 23, 1, 3 | lmodvsdir 20361 |
. . . 4
β’ ((π β LMod β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ) β§ (1rβπ) β (Baseβπ))) β ((π₯(+gβπΉ)π¦)( Β·π
βπ)(1rβπ)) = ((π₯( Β·π
βπ)(1rβπ))(+gβπ)(π¦( Β·π
βπ)(1rβπ)))) |
25 | 16, 17, 18, 22, 24 | syl13anc 1373 |
. . 3
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β ((π₯(+gβπΉ)π¦)( Β·π
βπ)(1rβπ)) = ((π₯( Β·π
βπ)(1rβπ))(+gβπ)(π¦( Β·π
βπ)(1rβπ)))) |
26 | 1, 3 | grpcl 18761 |
. . . . . 6
β’ ((πΉ β Grp β§ π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ)) β (π₯(+gβπΉ)π¦) β (BaseβπΉ)) |
27 | 26 | 3expb 1121 |
. . . . 5
β’ ((πΉ β Grp β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β (π₯(+gβπΉ)π¦) β (BaseβπΉ)) |
28 | 10, 27 | sylan 581 |
. . . 4
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β (π₯(+gβπΉ)π¦) β (BaseβπΉ)) |
29 | 14, 6, 1, 23, 19 | asclval 21299 |
. . . 4
β’ ((π₯(+gβπΉ)π¦) β (BaseβπΉ) β (π΄β(π₯(+gβπΉ)π¦)) = ((π₯(+gβπΉ)π¦)( Β·π
βπ)(1rβπ))) |
30 | 28, 29 | syl 17 |
. . 3
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β (π΄β(π₯(+gβπΉ)π¦)) = ((π₯(+gβπΉ)π¦)( Β·π
βπ)(1rβπ))) |
31 | 14, 6, 1, 23, 19 | asclval 21299 |
. . . . 5
β’ (π₯ β (BaseβπΉ) β (π΄βπ₯) = (π₯( Β·π
βπ)(1rβπ))) |
32 | 14, 6, 1, 23, 19 | asclval 21299 |
. . . . 5
β’ (π¦ β (BaseβπΉ) β (π΄βπ¦) = (π¦( Β·π
βπ)(1rβπ))) |
33 | 31, 32 | oveqan12d 7377 |
. . . 4
β’ ((π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ)) β ((π΄βπ₯)(+gβπ)(π΄βπ¦)) = ((π₯( Β·π
βπ)(1rβπ))(+gβπ)(π¦( Β·π
βπ)(1rβπ)))) |
34 | 33 | adantl 483 |
. . 3
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β ((π΄βπ₯)(+gβπ)(π΄βπ¦)) = ((π₯( Β·π
βπ)(1rβπ))(+gβπ)(π¦( Β·π
βπ)(1rβπ)))) |
35 | 25, 30, 34 | 3eqtr4d 2783 |
. 2
β’ ((π β§ (π₯ β (BaseβπΉ) β§ π¦ β (BaseβπΉ))) β (π΄β(π₯(+gβπΉ)π¦)) = ((π΄βπ₯)(+gβπ)(π΄βπ¦))) |
36 | 1, 2, 3, 4, 10, 13, 15, 35 | isghmd 19022 |
1
β’ (π β π΄ β (πΉ GrpHom π)) |