Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑛 = 0 → (𝑛 · 𝑋) = (0 · 𝑋)) |
2 | 1 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = 0 → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘(0 · 𝑋))) |
3 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = 0 → (𝑛 × (𝐹‘𝑋)) = (0 × (𝐹‘𝑋))) |
4 | 2, 3 | eqeq12d 2625 |
. . . . 5
⊢ (𝑛 = 0 → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘(0 · 𝑋)) = (0 × (𝐹‘𝑋)))) |
5 | 4 | imbi2d 329 |
. . . 4
⊢ (𝑛 = 0 → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0 · 𝑋)) = (0 × (𝐹‘𝑋))))) |
6 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑛 · 𝑋) = (𝑚 · 𝑋)) |
7 | 6 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘(𝑚 · 𝑋))) |
8 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑛 × (𝐹‘𝑋)) = (𝑚 × (𝐹‘𝑋))) |
9 | 7, 8 | eqeq12d 2625 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)))) |
10 | 9 | imbi2d 329 |
. . . 4
⊢ (𝑛 = 𝑚 → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋))))) |
11 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (𝑛 · 𝑋) = ((𝑚 + 1) · 𝑋)) |
12 | 11 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘((𝑚 + 1) · 𝑋))) |
13 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑛 × (𝐹‘𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))) |
14 | 12, 13 | eqeq12d 2625 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋)))) |
15 | 14 | imbi2d 329 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))))) |
16 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑛 · 𝑋) = (𝑁 · 𝑋)) |
17 | 16 | fveq2d 6107 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘(𝑁 · 𝑋))) |
18 | | oveq1 6556 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 × (𝐹‘𝑋)) = (𝑁 × (𝐹‘𝑋))) |
19 | 17, 18 | eqeq12d 2625 |
. . . . 5
⊢ (𝑛 = 𝑁 → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))) |
20 | 19 | imbi2d 329 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))))) |
21 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
22 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝐻) = (0g‘𝐻) |
23 | 21, 22 | mhm0 17166 |
. . . . . 6
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
24 | 23 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
25 | | mhmmulg.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
26 | | mhmmulg.s |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
27 | 25, 21, 26 | mulg0 17369 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
28 | 27 | adantl 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0g‘𝐺)) |
29 | 28 | fveq2d 6107 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0 · 𝑋)) = (𝐹‘(0g‘𝐺))) |
30 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) |
31 | 25, 30 | mhmf 17163 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐹:𝐵⟶(Base‘𝐻)) |
32 | 31 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ (Base‘𝐻)) |
33 | | mhmmulg.t |
. . . . . . 7
⊢ × =
(.g‘𝐻) |
34 | 30, 22, 33 | mulg0 17369 |
. . . . . 6
⊢ ((𝐹‘𝑋) ∈ (Base‘𝐻) → (0 × (𝐹‘𝑋)) = (0g‘𝐻)) |
35 | 32, 34 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (0 × (𝐹‘𝑋)) = (0g‘𝐻)) |
36 | 24, 29, 35 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0 · 𝑋)) = (0 × (𝐹‘𝑋))) |
37 | | oveq1 6556 |
. . . . . . 7
⊢ ((𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)) → ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
38 | | mhmrcl1 17161 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐺 ∈ Mnd) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝐺 ∈ Mnd) |
40 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
41 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
42 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
43 | 25, 26, 42 | mulgnn0p1 17375 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑚 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑚 + 1) · 𝑋) = ((𝑚 · 𝑋)(+g‘𝐺)𝑋)) |
44 | 39, 40, 41, 43 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) = ((𝑚 · 𝑋)(+g‘𝐺)𝑋)) |
45 | 44 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑚 + 1) · 𝑋)) = (𝐹‘((𝑚 · 𝑋)(+g‘𝐺)𝑋))) |
46 | | simpll 786 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝐹 ∈ (𝐺 MndHom 𝐻)) |
47 | 38 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → 𝐺 ∈ Mnd) |
48 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → 𝑚 ∈ ℕ0) |
49 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
50 | 25, 26 | mulgnn0cl 17381 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 𝑚 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) |
51 | 47, 48, 49, 50 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) |
52 | 51 | an32s 842 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑋) ∈ 𝐵) |
53 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘𝐻) = (+g‘𝐻) |
54 | 25, 42, 53 | mhmlin 17165 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝐹‘((𝑚 · 𝑋)(+g‘𝐺)𝑋)) = ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
55 | 46, 52, 41, 54 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑚 · 𝑋)(+g‘𝐺)𝑋)) = ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
56 | 45, 55 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
57 | | mhmrcl2 17162 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐻 ∈ Mnd) |
58 | 57 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝐻 ∈ Mnd) |
59 | 32 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑋) ∈ (Base‘𝐻)) |
60 | 30, 33, 53 | mulgnn0p1 17375 |
. . . . . . . . 9
⊢ ((𝐻 ∈ Mnd ∧ 𝑚 ∈ ℕ0
∧ (𝐹‘𝑋) ∈ (Base‘𝐻)) → ((𝑚 + 1) × (𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
61 | 58, 40, 59, 60 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) × (𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
62 | 56, 61 | eqeq12d 2625 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋)) ↔ ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋)))) |
63 | 37, 62 | syl5ibr 235 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋)))) |
64 | 63 | expcom 450 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
→ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → ((𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))))) |
65 | 64 | a2d 29 |
. . . 4
⊢ (𝑚 ∈ ℕ0
→ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋))) → ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))))) |
66 | 5, 10, 15, 20, 36, 65 | nn0ind 11348 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))) |
67 | 66 | 3impib 1254 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) |
68 | 67 | 3com12 1261 |
1
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) |