This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( 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 𝑀 ) )