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 = inv g ⁡ M
Assertion invlmhm ⊢ M ∈ LMod → I ∈ M LMHom M

Proof

Step Hyp Ref Expression
1 invlmhm.b ⊢ I = inv g ⁡ M
2 eqid ⊢ Base M = Base M
3 eqid ⊢ ⋅ M = ⋅ M
4 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
5 eqid ⊢ Base Scalar ⁡ M = Base Scalar ⁡ M
6 id ⊢ M ∈ LMod → M ∈ LMod
7 eqidd ⊢ M ∈ LMod → Scalar ⁡ M = Scalar ⁡ M
8 lmodabl ⊢ M ∈ LMod → M ∈ Abel
9 2 1 invghm ⊢ M ∈ Abel ↔ I ∈ M GrpHom M
10 8 9 sylib ⊢ M ∈ LMod → I ∈ M GrpHom M
11 2 4 3 1 5 lmodvsinv2 ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ Base M → x ⋅ M I ⁡ y = I ⁡ x ⋅ M y
12 11 eqcomd ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ Base M → I ⁡ x ⋅ M y = x ⋅ M I ⁡ y
13 12 3expb ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ Base M → I ⁡ x ⋅ M y = x ⋅ M I ⁡ y
14 2 3 3 4 4 5 6 6 7 10 13 islmhmd ⊢ M ∈ LMod → I ∈ M LMHom M