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