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

Metamath Proof Explorer

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 𝑀 ) )