Metamath Proof Explorer


Theorem idlmhm

Description: The identity function on a module is linear. (Contributed by Stefan O'Rear, 4-Sep-2015)

Ref Expression
Hypothesis idlmhm.b
|- B = ( Base ` M )
Assertion idlmhm
|- ( M e. LMod -> ( _I |` B ) e. ( M LMHom M ) )

Proof

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 ) )