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 ⊢ B = Base M
Assertion idlmhm ⊢ M ∈ LMod → I ↾ B ∈ M LMHom M

Proof

Step Hyp Ref Expression
1 idlmhm.b ⊢ B = Base M
2 eqid ⊢ ⋅ M = ⋅ M
3 eqid ⊢ Scalar ⁡ M = Scalar ⁡ M
4 eqid ⊢ Base Scalar ⁡ M = Base Scalar ⁡ M
5 id ⊢ M ∈ LMod → M ∈ LMod
6 eqidd ⊢ M ∈ LMod → Scalar ⁡ M = Scalar ⁡ M
7 lmodgrp ⊢ M ∈ LMod → M ∈ Grp
8 1 idghm ⊢ M ∈ Grp → I ↾ B ∈ M GrpHom M
9 7 8 syl ⊢ M ∈ LMod → I ↾ B ∈ M GrpHom M
10 1 3 2 4 lmodvscl ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ B → x ⋅ M y ∈ B
11 10 3expb ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ B → x ⋅ M y ∈ B
12 fvresi ⊢ x ⋅ M y ∈ B → I ↾ B ⁡ x ⋅ M y = x ⋅ M y
13 11 12 syl ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ B → I ↾ B ⁡ x ⋅ M y = x ⋅ M y
14 fvresi ⊢ y ∈ B → I ↾ B ⁡ y = y
15 14 ad2antll ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ B → I ↾ B ⁡ y = y
16 15 oveq2d ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ B → x ⋅ M I ↾ B ⁡ y = x ⋅ M y
17 13 16 eqtr4d ⊢ M ∈ LMod ∧ x ∈ Base Scalar ⁡ M ∧ y ∈ B → I ↾ B ⁡ x ⋅ M y = x ⋅ M I ↾ B ⁡ y
18 1 2 2 3 3 4 5 5 6 9 17 islmhmd ⊢ M ∈ LMod → I ↾ B ∈ M LMHom M