Step | Hyp | Ref
| Expression |
1 | | cmnmnd 18031 |
. . . 4
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
2 | 1 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ 𝐺 ∈
Mnd) |
3 | 2, 2 | jca 553 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝐺 ∈ Mnd ∧
𝐺 ∈
Mnd)) |
4 | | mulgmhm.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
5 | | mulgmhm.m |
. . . . . . 7
⊢ · =
(.g‘𝐺) |
6 | 4, 5 | mulgnn0cl 17381 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0
∧ 𝑥 ∈ 𝐵) → (𝑀 · 𝑥) ∈ 𝐵) |
7 | 1, 6 | syl3an1 1351 |
. . . . 5
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0
∧ 𝑥 ∈ 𝐵) → (𝑀 · 𝑥) ∈ 𝐵) |
8 | 7 | 3expa 1257 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ 𝑥 ∈ 𝐵) → (𝑀 · 𝑥) ∈ 𝐵) |
9 | | eqid 2610 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) |
10 | 8, 9 | fmptd 6292 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)):𝐵⟶𝐵) |
11 | | 3anass 1035 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ↔ (𝑀 ∈ ℕ0 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) |
12 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
13 | 4, 5, 12 | mulgnn0di 18054 |
. . . . . . 7
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 · (𝑦(+g‘𝐺)𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
14 | 11, 13 | sylan2br 492 |
. . . . . 6
⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵))) → (𝑀 · (𝑦(+g‘𝐺)𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
15 | 14 | anassrs 678 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑀 · (𝑦(+g‘𝐺)𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
16 | 4, 12 | mndcl 17124 |
. . . . . . . 8
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
17 | 16 | 3expb 1258 |
. . . . . . 7
⊢ ((𝐺 ∈ Mnd ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
18 | 2, 17 | sylan 487 |
. . . . . 6
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝐵) |
19 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑥 = (𝑦(+g‘𝐺)𝑧) → (𝑀 · 𝑥) = (𝑀 · (𝑦(+g‘𝐺)𝑧))) |
20 | | ovex 6577 |
. . . . . . 7
⊢ (𝑀 · (𝑦(+g‘𝐺)𝑧)) ∈ V |
21 | 19, 9, 20 | fvmpt 6191 |
. . . . . 6
⊢ ((𝑦(+g‘𝐺)𝑧) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (𝑀 · (𝑦(+g‘𝐺)𝑧))) |
22 | 18, 21 | syl 17 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (𝑀 · (𝑦(+g‘𝐺)𝑧))) |
23 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑀 · 𝑥) = (𝑀 · 𝑦)) |
24 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑀 · 𝑦) ∈ V |
25 | 23, 9, 24 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦) = (𝑀 · 𝑦)) |
26 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑀 · 𝑥) = (𝑀 · 𝑧)) |
27 | | ovex 6577 |
. . . . . . . 8
⊢ (𝑀 · 𝑧) ∈ V |
28 | 26, 9, 27 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧) = (𝑀 · 𝑧)) |
29 | 25, 28 | oveqan12d 6568 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
30 | 29 | adantl 481 |
. . . . 5
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) = ((𝑀 · 𝑦)(+g‘𝐺)(𝑀 · 𝑧))) |
31 | 15, 22, 30 | 3eqtr4d 2654 |
. . . 4
⊢ (((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧))) |
32 | 31 | ralrimivva 2954 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧))) |
33 | | eqid 2610 |
. . . . . 6
⊢
(0g‘𝐺) = (0g‘𝐺) |
34 | 4, 33 | mndidcl 17131 |
. . . . 5
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
35 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = (0g‘𝐺) → (𝑀 · 𝑥) = (𝑀 ·
(0g‘𝐺))) |
36 | | ovex 6577 |
. . . . . 6
⊢ (𝑀 ·
(0g‘𝐺))
∈ V |
37 | 35, 9, 36 | fvmpt 6191 |
. . . . 5
⊢
((0g‘𝐺) ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (𝑀 ·
(0g‘𝐺))) |
38 | 2, 34, 37 | 3syl 18 |
. . . 4
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (𝑀 ·
(0g‘𝐺))) |
39 | 4, 5, 33 | mulgnn0z 17390 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℕ0)
→ (𝑀 ·
(0g‘𝐺)) =
(0g‘𝐺)) |
40 | 1, 39 | sylan 487 |
. . . 4
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝑀 ·
(0g‘𝐺)) =
(0g‘𝐺)) |
41 | 38, 40 | eqtrd 2644 |
. . 3
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (0g‘𝐺)) |
42 | 10, 32, 41 | 3jca 1235 |
. 2
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (0g‘𝐺))) |
43 | 4, 4, 12, 12, 33, 33 | ismhm 17160 |
. 2
⊢ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺) ↔ ((𝐺 ∈ Mnd ∧ 𝐺 ∈ Mnd) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)):𝐵⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(𝑦(+g‘𝐺)𝑧)) = (((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑦)(+g‘𝐺)((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘𝑧)) ∧ ((𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥))‘(0g‘𝐺)) = (0g‘𝐺)))) |
44 | 3, 42, 43 | sylanbrc 695 |
1
⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0)
→ (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺)) |