Theorem idlmhm

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

	Ref	Expression
Hypothesis	idlmhm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion	idlmhm	⊢ ( 𝑀 ∈ LMod → ( I ↾ 𝐵 ) ∈ ( 𝑀 LMHom 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		idlmhm.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
3		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
4		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
5		id	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ LMod )
6		eqidd	⊢ ( 𝑀 ∈ LMod → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) )
7		lmodgrp	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
8	1	idghm	⊢ ( 𝑀 ∈ Grp → ( I ↾ 𝐵 ) ∈ ( 𝑀 GrpHom 𝑀 ) )
9	7 8	syl	⊢ ( 𝑀 ∈ LMod → ( I ↾ 𝐵 ) ∈ ( 𝑀 GrpHom 𝑀 ) )
10	1 3 2 4	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
11	10	3expb	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
12		fvresi	⊢ ( ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
13	11 12	syl	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
14		fvresi	⊢ ( 𝑦 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
15	14	ad2antll	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
16	15	oveq2d	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) )
17	13 16	eqtr4d	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ ( 𝑥 ( ·𝑠 ‘ 𝑀 ) 𝑦 ) ) = ( 𝑥 ( ·𝑠 ‘ 𝑀 ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) )
18	1 2 2 3 3 4 5 5 6 9 17	islmhmd	⊢ ( 𝑀 ∈ LMod → ( I ↾ 𝐵 ) ∈ ( 𝑀 LMHom 𝑀 ) )