Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . 4
β’ (π = β
β (πΊ Ξ£g
π) = (πΊ Ξ£g
β
)) |
2 | | eqid 2733 |
. . . . 5
β’
(0gβπΊ) = (0gβπΊ) |
3 | 2 | gsum0 18544 |
. . . 4
β’ (πΊ Ξ£g
β
) = (0gβπΊ) |
4 | 1, 3 | eqtrdi 2789 |
. . 3
β’ (π = β
β (πΊ Ξ£g
π) =
(0gβπΊ)) |
5 | 4 | eleq1d 2819 |
. 2
β’ (π = β
β ((πΊ Ξ£g
π) β π β (0gβπΊ) β π)) |
6 | | eqid 2733 |
. . . 4
β’
(BaseβπΊ) =
(BaseβπΊ) |
7 | | eqid 2733 |
. . . 4
β’
(+gβπΊ) = (+gβπΊ) |
8 | | submrcl 18618 |
. . . . 5
β’ (π β (SubMndβπΊ) β πΊ β Mnd) |
9 | 8 | ad2antrr 725 |
. . . 4
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β πΊ β Mnd) |
10 | | lennncl 14428 |
. . . . . . 7
β’ ((π β Word π β§ π β β
) β (β―βπ) β
β) |
11 | 10 | adantll 713 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (β―βπ) β
β) |
12 | | nnm1nn0 12459 |
. . . . . 6
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β0) |
13 | 11, 12 | syl 17 |
. . . . 5
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β ((β―βπ) β 1) β
β0) |
14 | | nn0uz 12810 |
. . . . 5
β’
β0 = (β€β₯β0) |
15 | 13, 14 | eleqtrdi 2844 |
. . . 4
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β ((β―βπ) β 1) β
(β€β₯β0)) |
16 | | wrdf 14413 |
. . . . . . 7
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
17 | 16 | ad2antlr 726 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π:(0..^(β―βπ))βΆπ) |
18 | 11 | nnzd 12531 |
. . . . . . . 8
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (β―βπ) β
β€) |
19 | | fzoval 13579 |
. . . . . . . 8
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β
(0..^(β―βπ)) =
(0...((β―βπ)
β 1))) |
21 | 20 | feq2d 6655 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (π:(0..^(β―βπ))βΆπ β π:(0...((β―βπ) β 1))βΆπ)) |
22 | 17, 21 | mpbid 231 |
. . . . 5
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π:(0...((β―βπ) β 1))βΆπ) |
23 | 6 | submss 18625 |
. . . . . 6
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
24 | 23 | ad2antrr 725 |
. . . . 5
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π β (BaseβπΊ)) |
25 | 22, 24 | fssd 6687 |
. . . 4
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π:(0...((β―βπ) β 1))βΆ(BaseβπΊ)) |
26 | 6, 7, 9, 15, 25 | gsumval2 18546 |
. . 3
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (πΊ Ξ£g π) =
(seq0((+gβπΊ), π)β((β―βπ) β 1))) |
27 | 22 | ffvelcdmda 7036 |
. . . 4
β’ ((((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β§ π₯ β (0...((β―βπ) β 1))) β (πβπ₯) β π) |
28 | 7 | submcl 18628 |
. . . . . 6
β’ ((π β (SubMndβπΊ) β§ π₯ β π β§ π¦ β π) β (π₯(+gβπΊ)π¦) β π) |
29 | 28 | 3expb 1121 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΊ)π¦) β π) |
30 | 29 | ad4ant14 751 |
. . . 4
β’ ((((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΊ)π¦) β π) |
31 | 15, 27, 30 | seqcl 13934 |
. . 3
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β
(seq0((+gβπΊ), π)β((β―βπ) β 1)) β π) |
32 | 26, 31 | eqeltrd 2834 |
. 2
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (πΊ Ξ£g π) β π) |
33 | 2 | subm0cl 18627 |
. . 3
β’ (π β (SubMndβπΊ) β
(0gβπΊ)
β π) |
34 | 33 | adantr 482 |
. 2
β’ ((π β (SubMndβπΊ) β§ π β Word π) β (0gβπΊ) β π) |
35 | 5, 32, 34 | pm2.61ne 3027 |
1
β’ ((π β (SubMndβπΊ) β§ π β Word π) β (πΊ Ξ£g π) β π) |