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