Step | Hyp | Ref
| Expression |
1 | | lmodvslmhm.k |
. 2
β’ πΎ = (BaseβπΉ) |
2 | | lmodvslmhm.v |
. 2
β’ π = (Baseβπ) |
3 | | eqid 2733 |
. 2
β’
(+gβπΉ) = (+gβπΉ) |
4 | | eqid 2733 |
. 2
β’
(+gβπ) = (+gβπ) |
5 | | lmodvslmhm.f |
. . . 4
β’ πΉ = (Scalarβπ) |
6 | 5 | lmodfgrp 20345 |
. . 3
β’ (π β LMod β πΉ β Grp) |
7 | 6 | adantr 482 |
. 2
β’ ((π β LMod β§ π β π) β πΉ β Grp) |
8 | | lmodgrp 20343 |
. . 3
β’ (π β LMod β π β Grp) |
9 | 8 | adantr 482 |
. 2
β’ ((π β LMod β§ π β π) β π β Grp) |
10 | | lmodvslmhm.s |
. . . . . 6
β’ Β· = (
Β·π βπ) |
11 | 2, 5, 10, 1 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ π₯ β πΎ β§ π β π) β (π₯ Β· π) β π) |
12 | 11 | 3expa 1119 |
. . . 4
β’ (((π β LMod β§ π₯ β πΎ) β§ π β π) β (π₯ Β· π) β π) |
13 | 12 | an32s 651 |
. . 3
β’ (((π β LMod β§ π β π) β§ π₯ β πΎ) β (π₯ Β· π) β π) |
14 | | eqid 2733 |
. . 3
β’ (π₯ β πΎ β¦ (π₯ Β· π)) = (π₯ β πΎ β¦ (π₯ Β· π)) |
15 | 13, 14 | fmptd 7063 |
. 2
β’ ((π β LMod β§ π β π) β (π₯ β πΎ β¦ (π₯ Β· π)):πΎβΆπ) |
16 | | simpll 766 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β π β LMod) |
17 | | simprl 770 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β π β πΎ) |
18 | | simprr 772 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β π β πΎ) |
19 | | simplr 768 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β π β π) |
20 | 2, 4, 5, 10, 1, 3 | lmodvsdir 20361 |
. . . 4
β’ ((π β LMod β§ (π β πΎ β§ π β πΎ β§ π β π)) β ((π(+gβπΉ)π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
21 | 16, 17, 18, 19, 20 | syl13anc 1373 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β ((π(+gβπΉ)π) Β· π) = ((π Β· π)(+gβπ)(π Β· π))) |
22 | 14 | a1i 11 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β (π₯ β πΎ β¦ (π₯ Β· π)) = (π₯ β πΎ β¦ (π₯ Β· π))) |
23 | | simpr 486 |
. . . . 5
β’ ((((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β§ π₯ = (π(+gβπΉ)π)) β π₯ = (π(+gβπΉ)π)) |
24 | 23 | oveq1d 7373 |
. . . 4
β’ ((((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β§ π₯ = (π(+gβπΉ)π)) β (π₯ Β· π) = ((π(+gβπΉ)π) Β· π)) |
25 | 5, 1, 3 | lmodacl 20348 |
. . . . . 6
β’ ((π β LMod β§ π β πΎ β§ π β πΎ) β (π(+gβπΉ)π) β πΎ) |
26 | 25 | 3expb 1121 |
. . . . 5
β’ ((π β LMod β§ (π β πΎ β§ π β πΎ)) β (π(+gβπΉ)π) β πΎ) |
27 | 26 | adantlr 714 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β (π(+gβπΉ)π) β πΎ) |
28 | | ovexd 7393 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β ((π(+gβπΉ)π) Β· π) β V) |
29 | 22, 24, 27, 28 | fvmptd 6956 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β ((π₯ β πΎ β¦ (π₯ Β· π))β(π(+gβπΉ)π)) = ((π(+gβπΉ)π) Β· π)) |
30 | | simpr 486 |
. . . . . 6
β’ ((((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β§ π₯ = π) β π₯ = π) |
31 | 30 | oveq1d 7373 |
. . . . 5
β’ ((((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β§ π₯ = π) β (π₯ Β· π) = (π Β· π)) |
32 | | ovexd 7393 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β (π Β· π) β V) |
33 | 22, 31, 17, 32 | fvmptd 6956 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β ((π₯ β πΎ β¦ (π₯ Β· π))βπ) = (π Β· π)) |
34 | | simpr 486 |
. . . . . 6
β’ ((((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β§ π₯ = π) β π₯ = π) |
35 | 34 | oveq1d 7373 |
. . . . 5
β’ ((((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β§ π₯ = π) β (π₯ Β· π) = (π Β· π)) |
36 | | ovexd 7393 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β (π Β· π) β V) |
37 | 22, 35, 18, 36 | fvmptd 6956 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β ((π₯ β πΎ β¦ (π₯ Β· π))βπ) = (π Β· π)) |
38 | 33, 37 | oveq12d 7376 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β (((π₯ β πΎ β¦ (π₯ Β· π))βπ)(+gβπ)((π₯ β πΎ β¦ (π₯ Β· π))βπ)) = ((π Β· π)(+gβπ)(π Β· π))) |
39 | 21, 29, 38 | 3eqtr4d 2783 |
. 2
β’ (((π β LMod β§ π β π) β§ (π β πΎ β§ π β πΎ)) β ((π₯ β πΎ β¦ (π₯ Β· π))β(π(+gβπΉ)π)) = (((π₯ β πΎ β¦ (π₯ Β· π))βπ)(+gβπ)((π₯ β πΎ β¦ (π₯ Β· π))βπ))) |
40 | 1, 2, 3, 4, 7, 9, 15, 39 | isghmd 19022 |
1
β’ ((π β LMod β§ π β π) β (π₯ β πΎ β¦ (π₯ Β· π)) β (πΉ GrpHom π)) |