idlmhm

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

		Ref	Expression
	Hypothesis	idlmhm.b	$⊢ B = {Base}_{M}$
	Assertion	idlmhm	$⊢ M \in LMod \to {I ↾}_{B} \in (M LMHom M)$

Step	Hyp	Ref	Expression
1		idlmhm.b	$⊢ B = {Base}_{M}$
2		eqid	$⊢ \cdot_{M} = \cdot_{M}$
3		eqid	$⊢ Scalar (M) = Scalar (M)$
4		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
5		id	$⊢ M \in LMod \to M \in LMod$
6		eqidd	$⊢ M \in LMod \to Scalar (M) = Scalar (M)$
7		lmodgrp	$⊢ M \in LMod \to M \in Grp$
8	1	idghm	$⊢ M \in Grp \to {I ↾}_{B} \in (M GrpHom M)$
9	7 8	syl	$⊢ M \in LMod \to {I ↾}_{B} \in (M GrpHom M)$
10	1 3 2 4	lmodvscl	$⊢ (M \in LMod \land x \in {Base}_{Scalar (M)} \land y \in B) \to x \cdot_{M} y \in B$
11	10	3expb	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in B)) \to x \cdot_{M} y \in B$
12		fvresi	$⊢ x \cdot_{M} y \in B \to ({I ↾}_{B}) (x \cdot_{M} y) = x \cdot_{M} y$
13	11 12	syl	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in B)) \to ({I ↾}_{B}) (x \cdot_{M} y) = x \cdot_{M} y$
14		fvresi	$⊢ y \in B \to ({I ↾}_{B}) (y) = y$
15	14	ad2antll	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in B)) \to ({I ↾}_{B}) (y) = y$
16	15	oveq2d	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in B)) \to x \cdot_{M} ({I ↾}_{B}) (y) = x \cdot_{M} y$
17	13 16	eqtr4d	$⊢ (M \in LMod \land (x \in {Base}_{Scalar (M)} \land y \in B)) \to ({I ↾}_{B}) (x \cdot_{M} y) = x \cdot_{M} ({I ↾}_{B}) (y)$
18	1 2 2 3 3 4 5 5 6 9 17	islmhmd	$⊢ M \in LMod \to {I ↾}_{B} \in (M LMHom M)$

Metamath Proof Explorer