Step | Hyp | Ref
| Expression |
1 | | pwsdiaglmhm.b |
. 2
β’ π΅ = (Baseβπ
) |
2 | | eqid 2733 |
. 2
β’ (
Β·π βπ
) = ( Β·π
βπ
) |
3 | | eqid 2733 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2733 |
. 2
β’
(Scalarβπ
) =
(Scalarβπ
) |
5 | | eqid 2733 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2733 |
. 2
β’
(Baseβ(Scalarβπ
)) = (Baseβ(Scalarβπ
)) |
7 | | simpl 484 |
. 2
β’ ((π
β LMod β§ πΌ β π) β π
β LMod) |
8 | | pwsdiaglmhm.y |
. . 3
β’ π = (π
βs πΌ) |
9 | 8 | pwslmod 20446 |
. 2
β’ ((π
β LMod β§ πΌ β π) β π β LMod) |
10 | 8, 4 | pwssca 17383 |
. . 3
β’ ((π
β LMod β§ πΌ β π) β (Scalarβπ
) = (Scalarβπ)) |
11 | 10 | eqcomd 2739 |
. 2
β’ ((π
β LMod β§ πΌ β π) β (Scalarβπ) = (Scalarβπ
)) |
12 | | lmodgrp 20343 |
. . 3
β’ (π
β LMod β π
β Grp) |
13 | | pwsdiaglmhm.f |
. . . 4
β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) |
14 | 8, 1, 13 | pwsdiagghm 19041 |
. . 3
β’ ((π
β Grp β§ πΌ β π) β πΉ β (π
GrpHom π)) |
15 | 12, 14 | sylan 581 |
. 2
β’ ((π
β LMod β§ πΌ β π) β πΉ β (π
GrpHom π)) |
16 | | simplr 768 |
. . . 4
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β πΌ β π) |
17 | 1, 4, 2, 6 | lmodvscl 20354 |
. . . . . 6
β’ ((π
β LMod β§ π β
(Baseβ(Scalarβπ
)) β§ π β π΅) β (π( Β·π
βπ
)π) β π΅) |
18 | 17 | 3expb 1121 |
. . . . 5
β’ ((π
β LMod β§ (π β
(Baseβ(Scalarβπ
)) β§ π β π΅)) β (π( Β·π
βπ
)π) β π΅) |
19 | 18 | adantlr 714 |
. . . 4
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (π( Β·π
βπ
)π) β π΅) |
20 | 13 | fvdiagfn 8832 |
. . . 4
β’ ((πΌ β π β§ (π( Β·π
βπ
)π) β π΅) β (πΉβ(π( Β·π
βπ
)π)) = (πΌ Γ {(π( Β·π
βπ
)π)})) |
21 | 16, 19, 20 | syl2anc 585 |
. . 3
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (πΉβ(π( Β·π
βπ
)π)) = (πΌ Γ {(π( Β·π
βπ
)π)})) |
22 | 13 | fvdiagfn 8832 |
. . . . . 6
β’ ((πΌ β π β§ π β π΅) β (πΉβπ) = (πΌ Γ {π})) |
23 | 22 | ad2ant2l 745 |
. . . . 5
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (πΉβπ) = (πΌ Γ {π})) |
24 | 23 | oveq2d 7374 |
. . . 4
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (π( Β·π
βπ)(πΉβπ)) = (π( Β·π
βπ)(πΌ Γ {π}))) |
25 | | eqid 2733 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
26 | | simpll 766 |
. . . . 5
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β π
β LMod) |
27 | | simprl 770 |
. . . . 5
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β π β (Baseβ(Scalarβπ
))) |
28 | 8, 1, 25 | pwsdiagel 17384 |
. . . . . 6
β’ (((π
β LMod β§ πΌ β π) β§ π β π΅) β (πΌ Γ {π}) β (Baseβπ)) |
29 | 28 | adantrl 715 |
. . . . 5
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (πΌ Γ {π}) β (Baseβπ)) |
30 | 8, 25, 2, 3, 4, 6, 26, 16, 27, 29 | pwsvscafval 17381 |
. . . 4
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (π( Β·π
βπ)(πΌ Γ {π})) = ((πΌ Γ {π}) βf (
Β·π βπ
)(πΌ Γ {π}))) |
31 | | id 22 |
. . . . . 6
β’ (πΌ β π β πΌ β π) |
32 | | vex 3448 |
. . . . . . 7
β’ π β V |
33 | 32 | a1i 11 |
. . . . . 6
β’ (πΌ β π β π β V) |
34 | | vex 3448 |
. . . . . . 7
β’ π β V |
35 | 34 | a1i 11 |
. . . . . 6
β’ (πΌ β π β π β V) |
36 | 31, 33, 35 | ofc12 7646 |
. . . . 5
β’ (πΌ β π β ((πΌ Γ {π}) βf (
Β·π βπ
)(πΌ Γ {π})) = (πΌ Γ {(π( Β·π
βπ
)π)})) |
37 | 36 | ad2antlr 726 |
. . . 4
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β ((πΌ Γ {π}) βf (
Β·π βπ
)(πΌ Γ {π})) = (πΌ Γ {(π( Β·π
βπ
)π)})) |
38 | 24, 30, 37 | 3eqtrd 2777 |
. . 3
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (π( Β·π
βπ)(πΉβπ)) = (πΌ Γ {(π( Β·π
βπ
)π)})) |
39 | 21, 38 | eqtr4d 2776 |
. 2
β’ (((π
β LMod β§ πΌ β π) β§ (π β (Baseβ(Scalarβπ
)) β§ π β π΅)) β (πΉβ(π( Β·π
βπ
)π)) = (π( Β·π
βπ)(πΉβπ))) |
40 | 1, 2, 3, 4, 5, 6, 7, 9, 11, 15, 39 | islmhmd 20515 |
1
β’ ((π
β LMod β§ πΌ β π) β πΉ β (π
LMHom π)) |