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 \in LMod \to I \in (M LMHom M)$

Step	Hyp	Ref	Expression
1		invlmhm.b	$⊢ I = {inv}_{g} (M)$
2		eqid	$⊢ {Base}_{M} = {Base}_{M}$
3		eqid	$⊢ \cdot_{M} = \cdot_{M}$
4		eqid	$⊢ Scalar (M) = Scalar (M)$
5		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
6		id	$⊢ M \in LMod \to M \in LMod$
7		eqidd	$⊢ M \in LMod \to Scalar (M) = Scalar (M)$
8		lmodabl	$⊢ M \in LMod \to M \in Abel$
9	2 1	invghm	$⊢ M \in Abel \leftrightarrow I \in (M GrpHom M)$
10	8 9	sylib	$⊢ M \in LMod \to I \in (M GrpHom M)$
11	2 4 3 1 5	lmodvsinv2	$⊢ (M \in LMod \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to x \cdot_{M} I (y) = I (x \cdot_{M} y)$
12	11	eqcomd	$⊢ (M \in LMod \land x \in {Base}_{Scalar (M)} \land y \in {Base}_{M}) \to I (x \cdot_{M} y) = x \cdot_{M} I (y)$
13	12	3expb	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in {Base}_{M})) \to I (x \cdot_{M} y) = x \cdot_{M} I (y)$
14	2 3 3 4 4 5 6 6 7 10 13	islmhmd	$⊢ M \in LMod \to I \in (M LMHom M)$

Metamath Proof Explorer