Step | Hyp | Ref
| Expression |
1 | | lmodvsghm.v |
. 2
β’ π = (Baseβπ) |
2 | | eqid 2733 |
. 2
β’
(+gβπ) = (+gβπ) |
3 | | lmodgrp 20343 |
. . 3
β’ (π β LMod β π β Grp) |
4 | 3 | adantr 482 |
. 2
β’ ((π β LMod β§ π
β πΎ) β π β Grp) |
5 | | lmodvsghm.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
6 | | lmodvsghm.s |
. . . . 5
β’ Β· = (
Β·π βπ) |
7 | | lmodvsghm.k |
. . . . 5
β’ πΎ = (BaseβπΉ) |
8 | 1, 5, 6, 7 | lmodvscl 20354 |
. . . 4
β’ ((π β LMod β§ π
β πΎ β§ π₯ β π) β (π
Β· π₯) β π) |
9 | 8 | 3expa 1119 |
. . 3
β’ (((π β LMod β§ π
β πΎ) β§ π₯ β π) β (π
Β· π₯) β π) |
10 | 9 | fmpttd 7064 |
. 2
β’ ((π β LMod β§ π
β πΎ) β (π₯ β π β¦ (π
Β· π₯)):πβΆπ) |
11 | 1, 2, 5, 6, 7 | lmodvsdi 20360 |
. . . . 5
β’ ((π β LMod β§ (π
β πΎ β§ π¦ β π β§ π§ β π)) β (π
Β· (π¦(+gβπ)π§)) = ((π
Β· π¦)(+gβπ)(π
Β· π§))) |
12 | 11 | 3exp2 1355 |
. . . 4
β’ (π β LMod β (π
β πΎ β (π¦ β π β (π§ β π β (π
Β· (π¦(+gβπ)π§)) = ((π
Β· π¦)(+gβπ)(π
Β· π§)))))) |
13 | 12 | imp43 429 |
. . 3
β’ (((π β LMod β§ π
β πΎ) β§ (π¦ β π β§ π§ β π)) β (π
Β· (π¦(+gβπ)π§)) = ((π
Β· π¦)(+gβπ)(π
Β· π§))) |
14 | 1, 2 | lmodvacl 20351 |
. . . . . 6
β’ ((π β LMod β§ π¦ β π β§ π§ β π) β (π¦(+gβπ)π§) β π) |
15 | 14 | 3expb 1121 |
. . . . 5
β’ ((π β LMod β§ (π¦ β π β§ π§ β π)) β (π¦(+gβπ)π§) β π) |
16 | 15 | adantlr 714 |
. . . 4
β’ (((π β LMod β§ π
β πΎ) β§ (π¦ β π β§ π§ β π)) β (π¦(+gβπ)π§) β π) |
17 | | oveq2 7366 |
. . . . 5
β’ (π₯ = (π¦(+gβπ)π§) β (π
Β· π₯) = (π
Β· (π¦(+gβπ)π§))) |
18 | | eqid 2733 |
. . . . 5
β’ (π₯ β π β¦ (π
Β· π₯)) = (π₯ β π β¦ (π
Β· π₯)) |
19 | | ovex 7391 |
. . . . 5
β’ (π
Β· (π¦(+gβπ)π§)) β V |
20 | 17, 18, 19 | fvmpt 6949 |
. . . 4
β’ ((π¦(+gβπ)π§) β π β ((π₯ β π β¦ (π
Β· π₯))β(π¦(+gβπ)π§)) = (π
Β· (π¦(+gβπ)π§))) |
21 | 16, 20 | syl 17 |
. . 3
β’ (((π β LMod β§ π
β πΎ) β§ (π¦ β π β§ π§ β π)) β ((π₯ β π β¦ (π
Β· π₯))β(π¦(+gβπ)π§)) = (π
Β· (π¦(+gβπ)π§))) |
22 | | oveq2 7366 |
. . . . . 6
β’ (π₯ = π¦ β (π
Β· π₯) = (π
Β· π¦)) |
23 | | ovex 7391 |
. . . . . 6
β’ (π
Β· π¦) β V |
24 | 22, 18, 23 | fvmpt 6949 |
. . . . 5
β’ (π¦ β π β ((π₯ β π β¦ (π
Β· π₯))βπ¦) = (π
Β· π¦)) |
25 | | oveq2 7366 |
. . . . . 6
β’ (π₯ = π§ β (π
Β· π₯) = (π
Β· π§)) |
26 | | ovex 7391 |
. . . . . 6
β’ (π
Β· π§) β V |
27 | 25, 18, 26 | fvmpt 6949 |
. . . . 5
β’ (π§ β π β ((π₯ β π β¦ (π
Β· π₯))βπ§) = (π
Β· π§)) |
28 | 24, 27 | oveqan12d 7377 |
. . . 4
β’ ((π¦ β π β§ π§ β π) β (((π₯ β π β¦ (π
Β· π₯))βπ¦)(+gβπ)((π₯ β π β¦ (π
Β· π₯))βπ§)) = ((π
Β· π¦)(+gβπ)(π
Β· π§))) |
29 | 28 | adantl 483 |
. . 3
β’ (((π β LMod β§ π
β πΎ) β§ (π¦ β π β§ π§ β π)) β (((π₯ β π β¦ (π
Β· π₯))βπ¦)(+gβπ)((π₯ β π β¦ (π
Β· π₯))βπ§)) = ((π
Β· π¦)(+gβπ)(π
Β· π§))) |
30 | 13, 21, 29 | 3eqtr4d 2783 |
. 2
β’ (((π β LMod β§ π
β πΎ) β§ (π¦ β π β§ π§ β π)) β ((π₯ β π β¦ (π
Β· π₯))β(π¦(+gβπ)π§)) = (((π₯ β π β¦ (π
Β· π₯))βπ¦)(+gβπ)((π₯ β π β¦ (π
Β· π₯))βπ§))) |
31 | 1, 1, 2, 2, 4, 4, 10, 30 | isghmd 19022 |
1
β’ ((π β LMod β§ π
β πΎ) β (π₯ β π β¦ (π
Β· π₯)) β (π GrpHom π)) |