Step | Hyp | Ref
| Expression |
1 | | idlmhm.b |
. 2
β’ π΅ = (Baseβπ) |
2 | | eqid 2737 |
. 2
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2737 |
. 2
β’
(Scalarβπ) =
(Scalarβπ) |
4 | | eqid 2737 |
. 2
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
5 | | id 22 |
. 2
β’ (π β LMod β π β LMod) |
6 | | eqidd 2738 |
. 2
β’ (π β LMod β
(Scalarβπ) =
(Scalarβπ)) |
7 | | lmodgrp 20345 |
. . 3
β’ (π β LMod β π β Grp) |
8 | 1 | idghm 19030 |
. . 3
β’ (π β Grp β ( I βΎ
π΅) β (π GrpHom π)) |
9 | 7, 8 | syl 17 |
. 2
β’ (π β LMod β ( I βΎ
π΅) β (π GrpHom π)) |
10 | 1, 3, 2, 4 | lmodvscl 20355 |
. . . . 5
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅) β (π₯( Β·π
βπ)π¦) β π΅) |
11 | 10 | 3expb 1121 |
. . . 4
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅)) β (π₯( Β·π
βπ)π¦) β π΅) |
12 | | fvresi 7124 |
. . . 4
β’ ((π₯(
Β·π βπ)π¦) β π΅ β (( I βΎ π΅)β(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)π¦)) |
13 | 11, 12 | syl 17 |
. . 3
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅)) β (( I βΎ π΅)β(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)π¦)) |
14 | | fvresi 7124 |
. . . . 5
β’ (π¦ β π΅ β (( I βΎ π΅)βπ¦) = π¦) |
15 | 14 | ad2antll 728 |
. . . 4
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅)) β (( I βΎ π΅)βπ¦) = π¦) |
16 | 15 | oveq2d 7378 |
. . 3
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅)) β (π₯( Β·π
βπ)(( I βΎ π΅)βπ¦)) = (π₯( Β·π
βπ)π¦)) |
17 | 13, 16 | eqtr4d 2780 |
. 2
β’ ((π β LMod β§ (π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β π΅)) β (( I βΎ π΅)β(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(( I βΎ π΅)βπ¦))) |
18 | 1, 2, 2, 3, 3, 4, 5, 5, 6, 9, 17 | islmhmd 20516 |
1
β’ (π β LMod β ( I βΎ
π΅) β (π LMHom π)) |