Step | Hyp | Ref
| Expression |
1 | | cmnmnd 18562 |
. . . 4
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
2 | 1 | adantr 474 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ 𝐺 ∈
Mnd) |
3 | 2, 2 | jca 509 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝐺 ∈ Mnd ∧
𝐺 ∈
Mnd)) |
4 | | mulgmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
5 | | mulgmhm.m |
. . . . . . 7
⊢ · =
(.g‘𝐺) |
6 | 4, 5 | mulgnn0cl 17912 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0
∧ 𝑥 ∈ 𝐵) → (𝑀 · 𝑥) ∈ 𝐵) |
7 | 1, 6 | syl3an1 1208 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0
∧ 𝑥 ∈ 𝐵) → (𝑀 · 𝑥) ∈ 𝐵) |
8 | 7 | 3expa 1153 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈ 𝐵) → (𝑀 · 𝑥) ∈ 𝐵) |
9 | 8 | fmpttd 6635 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)):𝐵⟶𝐵) |
10 | | 3anass 1122 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑀 ∈ ℕ0 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
11 | | eqid 2826 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
12 | 4, 5, 11 | mulgnn0di 18585 |
. . . . . . 7
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 · (𝑦(+g‘𝐺)𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
13 | 10, 12 | sylan2br 590 |
. . . . . 6
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) → (𝑀 · (𝑦(+g‘𝐺)𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
14 | 13 | anassrs 461 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 · (𝑦(+g‘𝐺)𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
15 | 4, 11 | mndcl 17655 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
16 | 15 | 3expb 1155 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
17 | 2, 16 | sylan 577 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
18 | | oveq2 6914 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (𝑀 · 𝑥) = (𝑀 · (𝑦(+g‘𝐺)𝑧))) |
19 | | eqid 2826 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) |
20 | | ovex 6938 |
. . . . . . 7
⊢ (𝑀 · (𝑦(+g‘𝐺)𝑧)) ∈ V |
21 | 18, 19, 20 | fvmpt 6530 |
. . . . . 6
⊢ ((𝑦(+g‘𝐺)𝑧) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (𝑀 · (𝑦(+g‘𝐺)𝑧))) |
22 | 17, 21 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (𝑀 · (𝑦(+g‘𝐺)𝑧))) |
23 | | oveq2 6914 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑀 · 𝑥) = (𝑀 · 𝑦)) |
24 | | ovex 6938 |
. . . . . . . 8
⊢ (𝑀 · 𝑦) ∈ V |
25 | 23, 19, 24 | fvmpt 6530 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦) = (𝑀 · 𝑦)) |
26 | | oveq2 6914 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑀 · 𝑥) = (𝑀 · 𝑧)) |
27 | | ovex 6938 |
. . . . . . . 8
⊢ (𝑀 · 𝑧) ∈ V |
28 | 26, 19, 27 | fvmpt 6530 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧) = (𝑀 · 𝑧)) |
29 | 25, 28 | oveqan12d 6925 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
30 | 29 | adantl 475 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
31 | 14, 22, 30 | 3eqtr4d 2872 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧))) |
32 | 31 | ralrimivva 3181 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧))) |
33 | | eqid 2826 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
34 | 4, 33 | mndidcl 17662 |
. . . . 5
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
35 | | oveq2 6914 |
. . . . . 6
⊢ (𝑥 = (0g‘𝐺) → (𝑀 · 𝑥) = (𝑀 ·
(0g‘𝐺))) |
36 | | ovex 6938 |
. . . . . 6
⊢ (𝑀 ·
(0g‘𝐺))
∈ V |
37 | 35, 19, 36 | fvmpt 6530 |
. . . . 5
⊢
((0g‘𝐺) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (𝑀 ·
(0g‘𝐺))) |
38 | 2, 34, 37 | 3syl 18 |
. . . 4
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (𝑀 ·
(0g‘𝐺))) |
39 | 4, 5, 33 | mulgnn0z 17921 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0)
→ (𝑀 ·
(0g‘𝐺)) =
(0g‘𝐺)) |
40 | 1, 39 | sylan 577 |
. . . 4
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝑀 ·
(0g‘𝐺)) =
(0g‘𝐺)) |
41 | 38, 40 | eqtrd 2862 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (0g‘𝐺)) |
42 | 9, 32, 41 | 3jca 1164 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (0g‘𝐺))) |
43 | 4, 4, 11, 11, 33, 33 | ismhm 17691 |
. 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺) ↔ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (0g‘𝐺)))) |
44 | 3, 42, 43 | sylanbrc 580 |
1
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺)) |