Step | Hyp | Ref
| Expression |
1 | | sgrpmgm 12812 |
. . . . . 6
β’ (πΊ β Smgrp β πΊ β Mgm) |
2 | | mulgnndir.b |
. . . . . . 7
β’ π΅ = (BaseβπΊ) |
3 | | mulgnndir.p |
. . . . . . 7
β’ + =
(+gβπΊ) |
4 | 2, 3 | mgmcl 12777 |
. . . . . 6
β’ ((πΊ β Mgm β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) |
5 | 1, 4 | syl3an1 1271 |
. . . . 5
β’ ((πΊ β Smgrp β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) |
6 | 5 | 3expb 1204 |
. . . 4
β’ ((πΊ β Smgrp β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
7 | 6 | adantlr 477 |
. . 3
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ + π¦) β π΅) |
8 | 2, 3 | sgrpass 12813 |
. . . 4
β’ ((πΊ β Smgrp β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
9 | 8 | adantlr 477 |
. . 3
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) |
10 | | simpr2 1004 |
. . . . . 6
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β β) |
11 | | nnuz 9562 |
. . . . . 6
β’ β =
(β€β₯β1) |
12 | 10, 11 | eleqtrdi 2270 |
. . . . 5
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β
(β€β₯β1)) |
13 | | simpr1 1003 |
. . . . . 6
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β β) |
14 | 13 | nnzd 9373 |
. . . . 5
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β β€) |
15 | | eluzadd 9555 |
. . . . 5
β’ ((π β
(β€β₯β1) β§ π β β€) β (π + π) β (β€β₯β(1 +
π))) |
16 | 12, 14, 15 | syl2anc 411 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π + π) β (β€β₯β(1 +
π))) |
17 | 13 | nncnd 8932 |
. . . . 5
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β β) |
18 | 10 | nncnd 8932 |
. . . . 5
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β β) |
19 | 17, 18 | addcomd 8107 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π + π) = (π + π)) |
20 | | ax-1cn 7903 |
. . . . . 6
β’ 1 β
β |
21 | | addcom 8093 |
. . . . . 6
β’ ((π β β β§ 1 β
β) β (π + 1) =
(1 + π)) |
22 | 17, 20, 21 | sylancl 413 |
. . . . 5
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π + 1) = (1 + π)) |
23 | 22 | fveq2d 5519 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β
(β€β₯β(π + 1)) = (β€β₯β(1 +
π))) |
24 | 16, 19, 23 | 3eltr4d 2261 |
. . 3
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π + π) β
(β€β₯β(π + 1))) |
25 | 13, 11 | eleqtrdi 2270 |
. . 3
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β
(β€β₯β1)) |
26 | | simpr3 1005 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β π β π΅) |
27 | 11, 26 | ialgrlemconst 12042 |
. . 3
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π₯ β (β€β₯β1))
β ((β Γ {π})βπ₯) β π΅) |
28 | 7, 9, 24, 25, 27 | seq3split 10478 |
. 2
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (seq1( + , (β Γ {π}))β(π + π)) = ((seq1( + , (β Γ {π}))βπ) + (seq(π + 1)( + , (β Γ {π}))β(π + π)))) |
29 | 13, 10 | nnaddcld 8966 |
. . 3
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π + π) β β) |
30 | | mulgnndir.t |
. . . 4
β’ Β· =
(.gβπΊ) |
31 | | eqid 2177 |
. . . 4
β’ seq1(
+ ,
(β Γ {π})) =
seq1( + ,
(β Γ {π})) |
32 | 2, 3, 30, 31 | mulgnn 12988 |
. . 3
β’ (((π + π) β β β§ π β π΅) β ((π + π) Β· π) = (seq1( + , (β Γ {π}))β(π + π))) |
33 | 29, 26, 32 | syl2anc 411 |
. 2
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β ((π + π) Β· π) = (seq1( + , (β Γ {π}))β(π + π))) |
34 | 2, 3, 30, 31 | mulgnn 12988 |
. . . 4
β’ ((π β β β§ π β π΅) β (π Β· π) = (seq1( + , (β Γ {π}))βπ)) |
35 | 13, 26, 34 | syl2anc 411 |
. . 3
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π Β· π) = (seq1( + , (β Γ {π}))βπ)) |
36 | | elfznn 10053 |
. . . . . . 7
β’ (π₯ β (1...π) β π₯ β β) |
37 | | fvconst2g 5730 |
. . . . . . 7
β’ ((π β π΅ β§ π₯ β β) β ((β Γ
{π})βπ₯) = π) |
38 | 26, 36, 37 | syl2an 289 |
. . . . . 6
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π₯ β (1...π)) β ((β Γ {π})βπ₯) = π) |
39 | | nnaddcl 8938 |
. . . . . . . 8
β’ ((π₯ β β β§ π β β) β (π₯ + π) β β) |
40 | 36, 13, 39 | syl2anr 290 |
. . . . . . 7
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π₯ β (1...π)) β (π₯ + π) β β) |
41 | | fvconst2g 5730 |
. . . . . . 7
β’ ((π β π΅ β§ (π₯ + π) β β) β ((β Γ
{π})β(π₯ + π)) = π) |
42 | 26, 40, 41 | syl2an2r 595 |
. . . . . 6
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π₯ β (1...π)) β ((β Γ {π})β(π₯ + π)) = π) |
43 | 38, 42 | eqtr4d 2213 |
. . . . 5
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π₯ β (1...π)) β ((β Γ {π})βπ₯) = ((β Γ {π})β(π₯ + π))) |
44 | | elnnuz 9563 |
. . . . . . 7
β’ (π’ β β β π’ β
(β€β₯β1)) |
45 | 44 | biimpri 133 |
. . . . . 6
β’ (π’ β
(β€β₯β1) β π’ β β) |
46 | | fvconst2g 5730 |
. . . . . . . 8
β’ ((π β π΅ β§ π’ β β) β ((β Γ
{π})βπ’) = π) |
47 | | simpl 109 |
. . . . . . . 8
β’ ((π β π΅ β§ π’ β β) β π β π΅) |
48 | 46, 47 | eqeltrd 2254 |
. . . . . . 7
β’ ((π β π΅ β§ π’ β β) β ((β Γ
{π})βπ’) β π΅) |
49 | 48 | elexd 2750 |
. . . . . 6
β’ ((π β π΅ β§ π’ β β) β ((β Γ
{π})βπ’) β V) |
50 | 26, 45, 49 | syl2an 289 |
. . . . 5
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π’ β (β€β₯β1))
β ((β Γ {π})βπ’) β V) |
51 | | 1nn 8929 |
. . . . . . . . 9
β’ 1 β
β |
52 | 51 | a1i 9 |
. . . . . . . 8
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π’ β (β€β₯β(1 +
π))) β 1 β
β) |
53 | 13 | adantr 276 |
. . . . . . . 8
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π’ β (β€β₯β(1 +
π))) β π β
β) |
54 | 52, 53 | nnaddcld 8966 |
. . . . . . 7
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π’ β (β€β₯β(1 +
π))) β (1 + π) β
β) |
55 | | eluznn 9599 |
. . . . . . 7
β’ (((1 +
π) β β β§
π’ β
(β€β₯β(1 + π))) β π’ β β) |
56 | 54, 55 | sylancom 420 |
. . . . . 6
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π’ β (β€β₯β(1 +
π))) β π’ β
β) |
57 | 26, 56, 49 | syl2an2r 595 |
. . . . 5
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ π’ β (β€β₯β(1 +
π))) β ((β
Γ {π})βπ’) β V) |
58 | | simprl 529 |
. . . . . 6
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ (π’ β V β§ π£ β V)) β π’ β V) |
59 | | plusgslid 12570 |
. . . . . . . . 9
β’
(+g = Slot (+gβndx) β§
(+gβndx) β β) |
60 | 59 | slotex 12488 |
. . . . . . . 8
β’ (πΊ β Smgrp β
(+gβπΊ)
β V) |
61 | 3, 60 | eqeltrid 2264 |
. . . . . . 7
β’ (πΊ β Smgrp β + β
V) |
62 | 61 | ad2antrr 488 |
. . . . . 6
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ (π’ β V β§ π£ β V)) β + β V) |
63 | | simprr 531 |
. . . . . 6
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ (π’ β V β§ π£ β V)) β π£ β V) |
64 | | ovexg 5908 |
. . . . . 6
β’ ((π’ β V β§ + β V
β§ π£ β V) β
(π’ + π£) β V) |
65 | 58, 62, 63, 64 | syl3anc 1238 |
. . . . 5
β’ (((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β§ (π’ β V β§ π£ β V)) β (π’ + π£) β V) |
66 | 12, 14, 43, 50, 57, 65 | seq3shft2 10472 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (seq1( + , (β Γ {π}))βπ) = (seq(1 + π)( + , (β Γ {π}))β(π + π))) |
67 | 2, 3, 30, 31 | mulgnn 12988 |
. . . . 5
β’ ((π β β β§ π β π΅) β (π Β· π) = (seq1( + , (β Γ {π}))βπ)) |
68 | 10, 26, 67 | syl2anc 411 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π Β· π) = (seq1( + , (β Γ {π}))βπ)) |
69 | 22 | seqeq1d 10450 |
. . . . 5
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β seq(π + 1)( + , (β Γ {π})) = seq(1 + π)( + , (β Γ {π}))) |
70 | 69, 19 | fveq12d 5522 |
. . . 4
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (seq(π + 1)( + , (β Γ {π}))β(π + π)) = (seq(1 + π)( + , (β Γ {π}))β(π + π))) |
71 | 66, 68, 70 | 3eqtr4d 2220 |
. . 3
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β (π Β· π) = (seq(π + 1)( + , (β Γ {π}))β(π + π))) |
72 | 35, 71 | oveq12d 5892 |
. 2
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β ((π Β· π) + (π Β· π)) = ((seq1( + , (β Γ {π}))βπ) + (seq(π + 1)( + , (β Γ {π}))β(π + π)))) |
73 | 28, 33, 72 | 3eqtr4d 2220 |
1
β’ ((πΊ β Smgrp β§ (π β β β§ π β β β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π) + (π Β· π))) |