Step | Hyp | Ref
| Expression |
1 | | lmodvsghm.v |
. 2
⊢ 𝑉 = (Base‘𝑊) |
2 | | eqid 2737 |
. 2
⊢
(+g‘𝑊) = (+g‘𝑊) |
3 | | lmodgrp 19906 |
. . 3
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) |
4 | 3 | adantr 484 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → 𝑊 ∈ Grp) |
5 | | lmodvsghm.f |
. . . . 5
⊢ 𝐹 = (Scalar‘𝑊) |
6 | | lmodvsghm.s |
. . . . 5
⊢ · = (
·𝑠 ‘𝑊) |
7 | | lmodvsghm.k |
. . . . 5
⊢ 𝐾 = (Base‘𝐹) |
8 | 1, 5, 6, 7 | lmodvscl 19916 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ∧ 𝑥 ∈ 𝑉) → (𝑅 · 𝑥) ∈ 𝑉) |
9 | 8 | 3expa 1120 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) ∧ 𝑥 ∈ 𝑉) → (𝑅 · 𝑥) ∈ 𝑉) |
10 | 9 | fmpttd 6932 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥)):𝑉⟶𝑉) |
11 | 1, 2, 5, 6, 7 | lmodvsdi 19922 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑅 ∈ 𝐾 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑅 · (𝑦(+g‘𝑊)𝑧)) = ((𝑅 · 𝑦)(+g‘𝑊)(𝑅 · 𝑧))) |
12 | 11 | 3exp2 1356 |
. . . 4
⊢ (𝑊 ∈ LMod → (𝑅 ∈ 𝐾 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (𝑅 · (𝑦(+g‘𝑊)𝑧)) = ((𝑅 · 𝑦)(+g‘𝑊)(𝑅 · 𝑧)))))) |
13 | 12 | imp43 431 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑅 · (𝑦(+g‘𝑊)𝑧)) = ((𝑅 · 𝑦)(+g‘𝑊)(𝑅 · 𝑧))) |
14 | 1, 2 | lmodvacl 19913 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (𝑦(+g‘𝑊)𝑧) ∈ 𝑉) |
15 | 14 | 3expb 1122 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦(+g‘𝑊)𝑧) ∈ 𝑉) |
16 | 15 | adantlr 715 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦(+g‘𝑊)𝑧) ∈ 𝑉) |
17 | | oveq2 7221 |
. . . . 5
⊢ (𝑥 = (𝑦(+g‘𝑊)𝑧) → (𝑅 · 𝑥) = (𝑅 · (𝑦(+g‘𝑊)𝑧))) |
18 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥)) = (𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥)) |
19 | | ovex 7246 |
. . . . 5
⊢ (𝑅 · (𝑦(+g‘𝑊)𝑧)) ∈ V |
20 | 17, 18, 19 | fvmpt 6818 |
. . . 4
⊢ ((𝑦(+g‘𝑊)𝑧) ∈ 𝑉 → ((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘(𝑦(+g‘𝑊)𝑧)) = (𝑅 · (𝑦(+g‘𝑊)𝑧))) |
21 | 16, 20 | syl 17 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘(𝑦(+g‘𝑊)𝑧)) = (𝑅 · (𝑦(+g‘𝑊)𝑧))) |
22 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑅 · 𝑥) = (𝑅 · 𝑦)) |
23 | | ovex 7246 |
. . . . . 6
⊢ (𝑅 · 𝑦) ∈ V |
24 | 22, 18, 23 | fvmpt 6818 |
. . . . 5
⊢ (𝑦 ∈ 𝑉 → ((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑦) = (𝑅 · 𝑦)) |
25 | | oveq2 7221 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (𝑅 · 𝑥) = (𝑅 · 𝑧)) |
26 | | ovex 7246 |
. . . . . 6
⊢ (𝑅 · 𝑧) ∈ V |
27 | 25, 18, 26 | fvmpt 6818 |
. . . . 5
⊢ (𝑧 ∈ 𝑉 → ((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑧) = (𝑅 · 𝑧)) |
28 | 24, 27 | oveqan12d 7232 |
. . . 4
⊢ ((𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → (((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑦)(+g‘𝑊)((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑧)) = ((𝑅 · 𝑦)(+g‘𝑊)(𝑅 · 𝑧))) |
29 | 28 | adantl 485 |
. . 3
⊢ (((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑦)(+g‘𝑊)((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑧)) = ((𝑅 · 𝑦)(+g‘𝑊)(𝑅 · 𝑧))) |
30 | 13, 21, 29 | 3eqtr4d 2787 |
. 2
⊢ (((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘(𝑦(+g‘𝑊)𝑧)) = (((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑦)(+g‘𝑊)((𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥))‘𝑧))) |
31 | 1, 1, 2, 2, 4, 4, 10, 30 | isghmd 18631 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾) → (𝑥 ∈ 𝑉 ↦ (𝑅 · 𝑥)) ∈ (𝑊 GrpHom 𝑊)) |