Step |
Hyp |
Ref |
Expression |
1 |
|
idlmhm.b |
|- B = ( Base ` M ) |
2 |
|
eqid |
|- ( .s ` M ) = ( .s ` M ) |
3 |
|
eqid |
|- ( Scalar ` M ) = ( Scalar ` M ) |
4 |
|
eqid |
|- ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) ) |
5 |
|
id |
|- ( M e. LMod -> M e. LMod ) |
6 |
|
eqidd |
|- ( M e. LMod -> ( Scalar ` M ) = ( Scalar ` M ) ) |
7 |
|
lmodgrp |
|- ( M e. LMod -> M e. Grp ) |
8 |
1
|
idghm |
|- ( M e. Grp -> ( _I |` B ) e. ( M GrpHom M ) ) |
9 |
7 8
|
syl |
|- ( M e. LMod -> ( _I |` B ) e. ( M GrpHom M ) ) |
10 |
1 3 2 4
|
lmodvscl |
|- ( ( M e. LMod /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. B ) -> ( x ( .s ` M ) y ) e. B ) |
11 |
10
|
3expb |
|- ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. B ) ) -> ( x ( .s ` M ) y ) e. B ) |
12 |
|
fvresi |
|- ( ( x ( .s ` M ) y ) e. B -> ( ( _I |` B ) ` ( x ( .s ` M ) y ) ) = ( x ( .s ` M ) y ) ) |
13 |
11 12
|
syl |
|- ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. B ) ) -> ( ( _I |` B ) ` ( x ( .s ` M ) y ) ) = ( x ( .s ` M ) y ) ) |
14 |
|
fvresi |
|- ( y e. B -> ( ( _I |` B ) ` y ) = y ) |
15 |
14
|
ad2antll |
|- ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. B ) ) -> ( ( _I |` B ) ` y ) = y ) |
16 |
15
|
oveq2d |
|- ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. B ) ) -> ( x ( .s ` M ) ( ( _I |` B ) ` y ) ) = ( x ( .s ` M ) y ) ) |
17 |
13 16
|
eqtr4d |
|- ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. B ) ) -> ( ( _I |` B ) ` ( x ( .s ` M ) y ) ) = ( x ( .s ` M ) ( ( _I |` B ) ` y ) ) ) |
18 |
1 2 2 3 3 4 5 5 6 9 17
|
islmhmd |
|- ( M e. LMod -> ( _I |` B ) e. ( M LMHom M ) ) |