| Step | Hyp | Ref
| Expression |
| 1 | | sgrpmgm 18737 |
. . . . . 6
⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm) |
| 2 | | mulgnndir.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐺) |
| 3 | | mulgnndir.p |
. . . . . . 7
⊢ + =
(+g‘𝐺) |
| 4 | 2, 3 | mgmcl 18656 |
. . . . . 6
⊢ ((𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
| 5 | 1, 4 | syl3an1 1164 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) |
| 6 | 5 | 3expb 1121 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
| 7 | 6 | adantlr 715 |
. . 3
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵) |
| 8 | 2, 3 | sgrpass 18738 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 9 | 8 | adantlr 715 |
. . 3
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) |
| 10 | | simpr2 1196 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℕ) |
| 11 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 12 | 10, 11 | eleqtrdi 2851 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈
(ℤ≥‘1)) |
| 13 | | simpr1 1195 |
. . . . . 6
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℕ) |
| 14 | 13 | nnzd 12640 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℤ) |
| 15 | | eluzadd 12907 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(1 +
𝑀))) |
| 16 | 12, 14, 15 | syl2anc 584 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 + 𝑀) ∈ (ℤ≥‘(1 +
𝑀))) |
| 17 | 13 | nncnd 12282 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℂ) |
| 18 | 10 | nncnd 12282 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℂ) |
| 19 | 17, 18 | addcomd 11463 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) = (𝑁 + 𝑀)) |
| 20 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 21 | | addcom 11447 |
. . . . . 6
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑀 + 1) =
(1 + 𝑀)) |
| 22 | 17, 20, 21 | sylancl 586 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 1) = (1 + 𝑀)) |
| 23 | 22 | fveq2d 6910 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) →
(ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 +
𝑀))) |
| 24 | 16, 19, 23 | 3eltr4d 2856 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈
(ℤ≥‘(𝑀 + 1))) |
| 25 | 13, 11 | eleqtrdi 2851 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈
(ℤ≥‘1)) |
| 26 | | simpr3 1197 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑋 ∈ 𝐵) |
| 27 | | elfznn 13593 |
. . . . 5
⊢ (𝑥 ∈ (1...(𝑀 + 𝑁)) → 𝑥 ∈ ℕ) |
| 28 | | fvconst2g 7222 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑥 ∈ ℕ) → ((ℕ ×
{𝑋})‘𝑥) = 𝑋) |
| 29 | 26, 27, 28 | syl2an 596 |
. . . 4
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...(𝑀 + 𝑁))) → ((ℕ × {𝑋})‘𝑥) = 𝑋) |
| 30 | 26 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...(𝑀 + 𝑁))) → 𝑋 ∈ 𝐵) |
| 31 | 29, 30 | eqeltrd 2841 |
. . 3
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...(𝑀 + 𝑁))) → ((ℕ × {𝑋})‘𝑥) ∈ 𝐵) |
| 32 | 7, 9, 24, 25, 31 | seqsplit 14076 |
. 2
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))) |
| 33 | | nnaddcl 12289 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ) |
| 34 | 13, 10, 33 | syl2anc 584 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈ ℕ) |
| 35 | | mulgnndir.t |
. . . 4
⊢ · =
(.g‘𝐺) |
| 36 | | eqid 2737 |
. . . 4
⊢ seq1(
+ ,
(ℕ × {𝑋})) =
seq1( + ,
(ℕ × {𝑋})) |
| 37 | 2, 3, 35, 36 | mulgnn 19093 |
. . 3
⊢ (((𝑀 + 𝑁) ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ((𝑀 + 𝑁) · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))) |
| 38 | 34, 26, 37 | syl2anc 584 |
. 2
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))) |
| 39 | 2, 3, 35, 36 | mulgnn 19093 |
. . . 4
⊢ ((𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
| 40 | 13, 26, 39 | syl2anc 584 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀)) |
| 41 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
| 42 | 26, 41, 28 | syl2an 596 |
. . . . . 6
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘𝑥) = 𝑋) |
| 43 | 26 | adantr 480 |
. . . . . . 7
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → 𝑋 ∈ 𝐵) |
| 44 | | nnaddcl 12289 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑥 + 𝑀) ∈ ℕ) |
| 45 | 41, 13, 44 | syl2anr 597 |
. . . . . . 7
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → (𝑥 + 𝑀) ∈ ℕ) |
| 46 | | fvconst2g 7222 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐵 ∧ (𝑥 + 𝑀) ∈ ℕ) → ((ℕ ×
{𝑋})‘(𝑥 + 𝑀)) = 𝑋) |
| 47 | 43, 45, 46 | syl2anc 584 |
. . . . . 6
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘(𝑥 + 𝑀)) = 𝑋) |
| 48 | 42, 47 | eqtr4d 2780 |
. . . . 5
⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘𝑥) = ((ℕ × {𝑋})‘(𝑥 + 𝑀))) |
| 49 | 12, 14, 48 | seqshft2 14069 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq1( + , (ℕ × {𝑋}))‘𝑁) = (seq(1 + 𝑀)( + , (ℕ × {𝑋}))‘(𝑁 + 𝑀))) |
| 50 | 2, 3, 35, 36 | mulgnn 19093 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑁)) |
| 51 | 10, 26, 50 | syl2anc 584 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑁)) |
| 52 | 22 | seqeq1d 14048 |
. . . . 5
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → seq(𝑀 + 1)( + , (ℕ × {𝑋})) = seq(1 + 𝑀)( + , (ℕ × {𝑋}))) |
| 53 | 52, 19 | fveq12d 6913 |
. . . 4
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)) = (seq(1 + 𝑀)( + , (ℕ × {𝑋}))‘(𝑁 + 𝑀))) |
| 54 | 49, 51, 53 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) = (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))) |
| 55 | 40, 54 | oveq12d 7449 |
. 2
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))) |
| 56 | 32, 38, 55 | 3eqtr4d 2787 |
1
⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋))) |