| Step | Hyp | Ref
| Expression |
|---|
| 1 | | oveq2 7417 |
. . . 4
β’ (π = β
β (πΊ Ξ£g
π) = (πΊ Ξ£g
β
)) |
| 2 | | eqid 2733 |
. . . . 5
β’
(0gβπΊ) = (0gβπΊ) |
| 3 | 2 | gsum0 18603 |
. . . 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 18683 |
. . . . 5
β’ (π β (SubMndβπΊ) β πΊ β Mnd) |
| 9 | 8 | ad2antrr 725 |
. . . 4
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β πΊ β Mnd) |
| 10 | | lennncl 14484 |
. . . . . . 7
β’ ((π β Word π β§ π β β
) β (β―βπ) β
β) |
| 11 | 10 | adantll 713 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (β―βπ) β
β) |
| 12 | | nnm1nn0 12513 |
. . . . . 6
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β0) |
| 13 | 11, 12 | syl 17 |
. . . . 5
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β ((β―βπ) β 1) β
β0) |
| 14 | | nn0uz 12864 |
. . . . 5
β’
β0 = (β€β₯β0) |
| 15 | 13, 14 | eleqtrdi 2844 |
. . . 4
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β ((β―βπ) β 1) β
(β€β₯β0)) |
| 16 | | wrdf 14469 |
. . . . . . 7
β’ (π β Word π β π:(0..^(β―βπ))βΆπ) |
| 17 | 16 | ad2antlr 726 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π:(0..^(β―βπ))βΆπ) |
| 18 | 11 | nnzd 12585 |
. . . . . . . 8
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (β―βπ) β
β€) |
| 19 | | fzoval 13633 |
. . . . . . . 8
β’
((β―βπ)
β β€ β (0..^(β―βπ)) = (0...((β―βπ) β 1))) |
| 20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β
(0..^(β―βπ)) =
(0...((β―βπ)
β 1))) |
| 21 | 20 | feq2d 6704 |
. . . . . 6
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (π:(0..^(β―βπ))βΆπ β π:(0...((β―βπ) β 1))βΆπ)) |
| 22 | 17, 21 | mpbid 231 |
. . . . 5
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π:(0...((β―βπ) β 1))βΆπ) |
| 23 | 6 | submss 18690 |
. . . . . 6
β’ (π β (SubMndβπΊ) β π β (BaseβπΊ)) |
| 24 | 23 | ad2antrr 725 |
. . . . 5
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π β (BaseβπΊ)) |
| 25 | 22, 24 | fssd 6736 |
. . . 4
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β π:(0...((β―βπ) β 1))βΆ(BaseβπΊ)) |
| 26 | 6, 7, 9, 15, 25 | gsumval2 18605 |
. . 3
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (πΊ Ξ£g π) =
(seq0((+gβπΊ), π)β((β―βπ) β 1))) |
| 27 | 22 | ffvelcdmda 7087 |
. . . 4
β’ ((((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β§ π₯ β (0...((β―βπ) β 1))) β (πβπ₯) β π) |
| 28 | 7 | submcl 18693 |
. . . . . 6
β’ ((π β (SubMndβπΊ) β§ π₯ β π β§ π¦ β π) β (π₯(+gβπΊ)π¦) β π) |
| 29 | 28 | 3expb 1121 |
. . . . 5
β’ ((π β (SubMndβπΊ) β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΊ)π¦) β π) |
| 30 | 29 | ad4ant14 751 |
. . . 4
β’ ((((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΊ)π¦) β π) |
| 31 | 15, 27, 30 | seqcl 13988 |
. . 3
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β
(seq0((+gβπΊ), π)β((β―βπ) β 1)) β π) |
| 32 | 26, 31 | eqeltrd 2834 |
. 2
β’ (((π β (SubMndβπΊ) β§ π β Word π) β§ π β β
) β (πΊ Ξ£g π) β π) |
| 33 | 2 | subm0cl 18692 |
. . 3
β’ (π β (SubMndβπΊ) β
(0gβπΊ)
β π) |
| 34 | 33 | adantr 482 |
. 2
β’ ((π β (SubMndβπΊ) β§ π β Word π) β (0gβπΊ) β π) |
| 35 | 5, 32, 34 | pm2.61ne 3028 |
1
β’ ((π β (SubMndβπΊ) β§ π β Word π) β (πΊ Ξ£g π) β π) |
