Metamath Proof Explorer

Theorem invlmhm

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

Ref Expression
Hypothesis invlmhm.b 
|- I = ( invg ` M )
Assertion invlmhm 
|- ( M e. LMod -> I e. ( M LMHom M ) )

Proof

Step Hyp Ref Expression
1 invlmhm.b 
 |-  I = ( invg ` M )
2 eqid 
 |-  ( Base ` M ) = ( Base ` M )
3 eqid 
 |-  ( .s ` M ) = ( .s ` M )
4 eqid 
 |-  ( Scalar ` M ) = ( Scalar ` M )
5 eqid 
 |-  ( Base ` ( Scalar ` M ) ) = ( Base ` ( Scalar ` M ) )
6 id 
 |-  ( M e. LMod -> M e. LMod )
7 eqidd 
 |-  ( M e. LMod -> ( Scalar ` M ) = ( Scalar ` M ) )
8 lmodabl 
 |-  ( M e. LMod -> M e. Abel )
9 2 1 invghm 
 |-  ( M e. Abel <-> I e. ( M GrpHom M ) )
10 8 9 sylib 
 |-  ( M e. LMod -> I e. ( M GrpHom M ) )
11 2 4 3 1 5 lmodvsinv2 
 |-  ( ( M e. LMod /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( x ( .s ` M ) ( I ` y ) ) = ( I ` ( x ( .s ` M ) y ) ) )
12 11 eqcomd 
 |-  ( ( M e. LMod /\ x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) -> ( I ` ( x ( .s ` M ) y ) ) = ( x ( .s ` M ) ( I ` y ) ) )
13 12 3expb 
 |-  ( ( M e. LMod /\ ( x e. ( Base ` ( Scalar ` M ) ) /\ y e. ( Base ` M ) ) ) -> ( I ` ( x ( .s ` M ) y ) ) = ( x ( .s ` M ) ( I ` y ) ) )
14 2 3 3 4 4 5 6 6 7 10 13 islmhmd 
 |-  ( M e. LMod -> I e. ( M LMHom M ) )