Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑛 = 0 → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘(0 · 𝑋))) |
2 | | oveq1 7220 |
. . . . . 6
⊢ (𝑛 = 0 → (𝑛 × (𝐹‘𝑋)) = (0 × (𝐹‘𝑋))) |
3 | 1, 2 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 0 → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘(0 · 𝑋)) = (0 × (𝐹‘𝑋)))) |
4 | 3 | imbi2d 344 |
. . . 4
⊢ (𝑛 = 0 → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0 · 𝑋)) = (0 × (𝐹‘𝑋))))) |
5 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘(𝑚 · 𝑋))) |
6 | | oveq1 7220 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (𝑛 × (𝐹‘𝑋)) = (𝑚 × (𝐹‘𝑋))) |
7 | 5, 6 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)))) |
8 | 7 | imbi2d 344 |
. . . 4
⊢ (𝑛 = 𝑚 → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋))))) |
9 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘((𝑚 + 1) · 𝑋))) |
10 | | oveq1 7220 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → (𝑛 × (𝐹‘𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))) |
11 | 9, 10 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋)))) |
12 | 11 | imbi2d 344 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))))) |
13 | | fvoveq1 7236 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝐹‘(𝑛 · 𝑋)) = (𝐹‘(𝑁 · 𝑋))) |
14 | | oveq1 7220 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (𝑛 × (𝐹‘𝑋)) = (𝑁 × (𝐹‘𝑋))) |
15 | 13, 14 | eqeq12d 2753 |
. . . . 5
⊢ (𝑛 = 𝑁 → ((𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋)) ↔ (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))) |
16 | 15 | imbi2d 344 |
. . . 4
⊢ (𝑛 = 𝑁 → (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑛 · 𝑋)) = (𝑛 × (𝐹‘𝑋))) ↔ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))))) |
17 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐺) = (0g‘𝐺) |
18 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝐻) = (0g‘𝐻) |
19 | 17, 18 | mhm0 18226 |
. . . . . 6
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
20 | 19 | adantr 484 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0g‘𝐺)) = (0g‘𝐻)) |
21 | | mhmmulg.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
22 | | mhmmulg.s |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
23 | 21, 17, 22 | mulg0 18495 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
24 | 23 | adantl 485 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0g‘𝐺)) |
25 | 24 | fveq2d 6721 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0 · 𝑋)) = (𝐹‘(0g‘𝐺))) |
26 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐻) =
(Base‘𝐻) |
27 | 21, 26 | mhmf 18223 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐹:𝐵⟶(Base‘𝐻)) |
28 | 27 | ffvelrnda 6904 |
. . . . . 6
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ (Base‘𝐻)) |
29 | | mhmmulg.t |
. . . . . . 7
⊢ × =
(.g‘𝐻) |
30 | 26, 18, 29 | mulg0 18495 |
. . . . . 6
⊢ ((𝐹‘𝑋) ∈ (Base‘𝐻) → (0 × (𝐹‘𝑋)) = (0g‘𝐻)) |
31 | 28, 30 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (0 × (𝐹‘𝑋)) = (0g‘𝐻)) |
32 | 20, 25, 31 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(0 · 𝑋)) = (0 × (𝐹‘𝑋))) |
33 | | oveq1 7220 |
. . . . . . 7
⊢ ((𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)) → ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
34 | | mhmrcl1 18221 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐺 ∈ Mnd) |
35 | 34 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝐺 ∈ Mnd) |
36 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
37 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈ 𝐵) |
38 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(+g‘𝐺) = (+g‘𝐺) |
39 | 21, 22, 38 | mulgnn0p1 18503 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ 𝑚 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑚 + 1) · 𝑋) = ((𝑚 · 𝑋)(+g‘𝐺)𝑋)) |
40 | 35, 36, 37, 39 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · 𝑋) = ((𝑚 · 𝑋)(+g‘𝐺)𝑋)) |
41 | 40 | fveq2d 6721 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑚 + 1) · 𝑋)) = (𝐹‘((𝑚 · 𝑋)(+g‘𝐺)𝑋))) |
42 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝐹 ∈ (𝐺 MndHom 𝐻)) |
43 | 34 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → 𝐺 ∈ Mnd) |
44 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → 𝑚 ∈ ℕ0) |
45 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ 𝐵) |
46 | 21, 22 | mulgnn0cl 18508 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 𝑚 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) |
47 | 43, 44, 45, 46 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑚 ∈ ℕ0) ∧ 𝑋 ∈ 𝐵) → (𝑚 · 𝑋) ∈ 𝐵) |
48 | 47 | an32s 652 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝑚 · 𝑋) ∈ 𝐵) |
49 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(+g‘𝐻) = (+g‘𝐻) |
50 | 21, 38, 49 | mhmlin 18225 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ (𝑚 · 𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝐹‘((𝑚 · 𝑋)(+g‘𝐺)𝑋)) = ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
51 | 42, 48, 37, 50 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑚 · 𝑋)(+g‘𝐺)𝑋)) = ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
52 | 41, 51 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
53 | | mhmrcl2 18222 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐺 MndHom 𝐻) → 𝐻 ∈ Mnd) |
54 | 53 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝐻 ∈ Mnd) |
55 | 28 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑋) ∈ (Base‘𝐻)) |
56 | 26, 29, 49 | mulgnn0p1 18503 |
. . . . . . . . 9
⊢ ((𝐻 ∈ Mnd ∧ 𝑚 ∈ ℕ0
∧ (𝐹‘𝑋) ∈ (Base‘𝐻)) → ((𝑚 + 1) × (𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
57 | 54, 36, 55, 56 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) × (𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋))) |
58 | 52, 57 | eqeq12d 2753 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋)) ↔ ((𝐹‘(𝑚 · 𝑋))(+g‘𝐻)(𝐹‘𝑋)) = ((𝑚 × (𝐹‘𝑋))(+g‘𝐻)(𝐹‘𝑋)))) |
59 | 33, 58 | syl5ibr 249 |
. . . . . 6
⊢ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋)))) |
60 | 59 | expcom 417 |
. . . . 5
⊢ (𝑚 ∈ ℕ0
→ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → ((𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋)) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))))) |
61 | 60 | a2d 29 |
. . . 4
⊢ (𝑚 ∈ ℕ0
→ (((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑚 · 𝑋)) = (𝑚 × (𝐹‘𝑋))) → ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘((𝑚 + 1) · 𝑋)) = ((𝑚 + 1) × (𝐹‘𝑋))))) |
62 | 4, 8, 12, 16, 32, 61 | nn0ind 12272 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))) |
63 | 62 | 3impib 1118 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) |
64 | 63 | 3com12 1125 |
1
⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋))) |