Theorem invlmhm

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

	Ref	Expression
Hypothesis	invlmhm.b	⊢ 𝐼 = ( invg ‘ 𝑀 )
Assertion	invlmhm	⊢ ( 𝑀 ∈ LMod → 𝐼 ∈ ( 𝑀 LMHom 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		invlmhm.b	⊢ 𝐼 = ( invg ‘ 𝑀 )
2		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
4		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
5		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
6		id	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ LMod )
7		eqidd	⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) )
8		lmodabl	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Abel )
9	2 1	invghm	⊢ ( 𝑀 ∈ Abel ↔ 𝐼 ∈ ( 𝑀 GrpHom 𝑀 ) )
10	8 9	sylib	⊢ ( 𝑀 ∈ LMod → 𝐼 ∈ ( 𝑀 GrpHom 𝑀 ) )
11	2 4 3 1 5	lmodvsinv2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ‘ 𝑦 ) ) = ( 𝐼 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) )
12	11	eqcomd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐼 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ‘ 𝑦 ) ) )
13	12	3expb	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) → ( 𝐼 ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) ( 𝐼 ‘ 𝑦 ) ) )
14	2 3 3 4 4 5 6 6 7 10 13	islmhmd	⊢ ( 𝑀 ∈ LMod → 𝐼 ∈ ( 𝑀 LMHom 𝑀 ) )