Step | Hyp | Ref
| Expression |
1 | | mulgnndir.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐺) |
2 | | mulgnndir.p |
. . . . . 6
⊢ + =
(+g‘𝐺) |
3 | 1, 2 | mndcl 17124 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
4 | 3 | 3expb 1258 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
5 | 4 | adantlr 747 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
6 | 1, 2 | mndass 17125 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
7 | 6 | adantlr 747 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
8 | | simpr2 1061 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℕ) |
9 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
10 | 8, 9 | syl6eleq 2698 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈
(ℤ≥‘1)) |
11 | | simpr1 1060 |
. . . . . 6
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℕ) |
12 | 11 | nnzd 11357 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℤ) |
13 | | eluzadd 11592 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(1 +
𝑀))) |
14 | 10, 12, 13 | syl2anc 691 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 + 𝑀) ∈ (ℤ≥‘(1 +
𝑀))) |
15 | 11 | nncnd 10913 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℂ) |
16 | 8 | nncnd 10913 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℂ) |
17 | 15, 16 | addcomd 10117 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) = (𝑁 + 𝑀)) |
18 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
19 | | addcom 10101 |
. . . . . 6
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + 1) =
(1 + 𝑀)) |
20 | 15, 18, 19 | sylancl 693 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 1) = (1 + 𝑀)) |
21 | 20 | fveq2d 6107 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) →
(ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 +
𝑀))) |
22 | 14, 17, 21 | 3eltr4d 2703 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈
(ℤ≥‘(𝑀 + 1))) |
23 | 11, 9 | syl6eleq 2698 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈
(ℤ≥‘1)) |
24 | | simpr3 1062 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
25 | | elfznn 12241 |
. . . . 5
⊢ (𝑥 ∈ (1...(𝑀 + 𝑁)) → 𝑥 ∈ ℕ) |
26 | | fvconst2g 6372 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑥 ∈ ℕ) → ((ℕ ×
{𝑋})‘𝑥) = 𝑋) |
27 | 24, 25, 26 | syl2an 493 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...(𝑀 + 𝑁))) → ((ℕ × {𝑋})‘𝑥) = 𝑋) |
28 | 24 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...(𝑀 + 𝑁))) → 𝑋 ∈ 𝐵) |
29 | 27, 28 | eqeltrd 2688 |
. . 3
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...(𝑀 + 𝑁))) → ((ℕ × {𝑋})‘𝑥) ∈ 𝐵) |
30 | 5, 7, 22, 23, 29 | seqsplit 12696 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))) |
31 | | nnaddcl 10919 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
32 | 11, 8, 31 | syl2anc 691 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈ ℕ) |
33 | | mulgnndir.t |
. . . 4
⊢ · =
(.g‘𝐺) |
34 | | eqid 2610 |
. . . 4
⊢ seq1(
+ ,
(ℕ × {𝑋})) =
seq1( + ,
(ℕ × {𝑋})) |
35 | 1, 2, 33, 34 | mulgnn 17370 |
. . 3
⊢ (((𝑀 + 𝑁) ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ((𝑀 + 𝑁) · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))) |
36 | 32, 24, 35 | syl2anc 691 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))) |
37 | 1, 2, 33, 34 | mulgnn 17370 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
38 | 11, 24, 37 | syl2anc 691 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
39 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
40 | 24, 39, 26 | syl2an 493 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘𝑥) = 𝑋) |
41 | 24 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → 𝑋 ∈ 𝐵) |
42 | | nnaddcl 10919 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑥 + 𝑀) ∈ ℕ) |
43 | 39, 11, 42 | syl2anr 494 |
. . . . . . 7
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → (𝑥 + 𝑀) ∈ ℕ) |
44 | | fvconst2g 6372 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ (𝑥 + 𝑀) ∈ ℕ) → ((ℕ ×
{𝑋})‘(𝑥 + 𝑀)) = 𝑋) |
45 | 41, 43, 44 | syl2anc 691 |
. . . . . 6
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘(𝑥 + 𝑀)) = 𝑋) |
46 | 40, 45 | eqtr4d 2647 |
. . . . 5
⊢ (((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘𝑥) = ((ℕ × {𝑋})‘(𝑥 + 𝑀))) |
47 | 10, 12, 46 | seqshft2 12689 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq1( + , (ℕ × {𝑋}))‘𝑁) = (seq(1 + 𝑀)( + , (ℕ × {𝑋}))‘(𝑁 + 𝑀))) |
48 | 1, 2, 33, 34 | mulgnn 17370 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑁)) |
49 | 8, 24, 48 | syl2anc 691 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑁)) |
50 | 20 | seqeq1d 12669 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → seq(𝑀 + 1)( + , (ℕ × {𝑋})) = seq(1 + 𝑀)( + , (ℕ × {𝑋}))) |
51 | 50, 17 | fveq12d 6109 |
. . . 4
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)) = (seq(1 + 𝑀)( + , (ℕ × {𝑋}))‘(𝑁 + 𝑀))) |
52 | 47, 49, 51 | 3eqtr4d 2654 |
. . 3
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) = (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))) |
53 | 38, 52 | oveq12d 6567 |
. 2
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))) |
54 | 30, 36, 53 | 3eqtr4d 2654 |
1
⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |