Step | Hyp | Ref
| Expression |
1 | | simplr 768 |
. . . . 5
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β π£ β Word ran (pmTrspβπ·)) |
2 | | lencl 14427 |
. . . . . . . 8
β’ (π£ β Word ran
(pmTrspβπ·) β
(β―βπ£) β
β0) |
3 | 2 | ad2antlr 726 |
. . . . . . 7
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β (β―βπ£) β
β0) |
4 | 3 | nn0zd 12530 |
. . . . . 6
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β (β―βπ£) β
β€) |
5 | | simpr 486 |
. . . . . . . 8
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β π = (π Ξ£g π£)) |
6 | 5 | fveq2d 6847 |
. . . . . . 7
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β ((pmSgnβπ·)βπ) = ((pmSgnβπ·)β(π Ξ£g π£))) |
7 | | simplll 774 |
. . . . . . . 8
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β π· β Fin) |
8 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β π β π΄) |
9 | | cyc3genpm.a |
. . . . . . . . 9
β’ π΄ = (pmEvenβπ·) |
10 | 8, 9 | eleqtrdi 2844 |
. . . . . . . 8
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β π β (pmEvenβπ·)) |
11 | | cyc3genpm.s |
. . . . . . . . 9
β’ π = (SymGrpβπ·) |
12 | | eqid 2733 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
(pmSgnβπ·) =
(pmSgnβπ·) |
14 | 11, 12, 13 | psgnevpm 21009 |
. . . . . . . 8
β’ ((π· β Fin β§ π β (pmEvenβπ·)) β ((pmSgnβπ·)βπ) = 1) |
15 | 7, 10, 14 | syl2anc 585 |
. . . . . . 7
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β ((pmSgnβπ·)βπ) = 1) |
16 | | eqid 2733 |
. . . . . . . . 9
β’ ran
(pmTrspβπ·) = ran
(pmTrspβπ·) |
17 | 11, 16, 13 | psgnvalii 19296 |
. . . . . . . 8
β’ ((π· β Fin β§ π£ β Word ran
(pmTrspβπ·)) β
((pmSgnβπ·)β(π Ξ£g π£)) =
(-1β(β―βπ£))) |
18 | 7, 1, 17 | syl2anc 585 |
. . . . . . 7
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β ((pmSgnβπ·)β(π Ξ£g π£)) =
(-1β(β―βπ£))) |
19 | 6, 15, 18 | 3eqtr3rd 2782 |
. . . . . 6
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β
(-1β(β―βπ£))
= 1) |
20 | | m1exp1 16263 |
. . . . . . 7
β’
((β―βπ£)
β β€ β ((-1β(β―βπ£)) = 1 β 2 β₯ (β―βπ£))) |
21 | 20 | biimpa 478 |
. . . . . 6
β’
(((β―βπ£)
β β€ β§ (-1β(β―βπ£)) = 1) β 2 β₯ (β―βπ£)) |
22 | 4, 19, 21 | syl2anc 585 |
. . . . 5
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β 2 β₯
(β―βπ£)) |
23 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = β
β (π Ξ£g
π₯) = (π Ξ£g
β
)) |
24 | 23 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π₯ = β
β ((π Ξ£g
π₯) = (π Ξ£g π€) β (π Ξ£g β
) =
(π
Ξ£g π€))) |
25 | 24 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = β
β (βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€) β βπ€ β Word πΆ(π Ξ£g β
) =
(π
Ξ£g π€))) |
26 | 25 | imbi2d 341 |
. . . . . . 7
β’ (π₯ = β
β ((π· β Fin β βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€)) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g β
) =
(π
Ξ£g π€)))) |
27 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = π’ β (π Ξ£g π₯) = (π Ξ£g π’)) |
28 | 27 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π₯ = π’ β ((π Ξ£g π₯) = (π Ξ£g π€) β (π Ξ£g π’) = (π Ξ£g π€))) |
29 | 28 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = π’ β (βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€) β βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) |
30 | 29 | imbi2d 341 |
. . . . . . 7
β’ (π₯ = π’ β ((π· β Fin β βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€)) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€)))) |
31 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = (π’ ++ β¨βππββ©) β (π Ξ£g π₯) = (π Ξ£g (π’ ++ β¨βππββ©))) |
32 | 31 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π₯ = (π’ ++ β¨βππββ©) β ((π Ξ£g π₯) = (π Ξ£g π€) β (π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€))) |
33 | 32 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = (π’ ++ β¨βππββ©) β (βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€) β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€))) |
34 | 33 | imbi2d 341 |
. . . . . . 7
β’ (π₯ = (π’ ++ β¨βππββ©) β ((π· β Fin β βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€)) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€)))) |
35 | | oveq2 7366 |
. . . . . . . . . 10
β’ (π₯ = π£ β (π Ξ£g π₯) = (π Ξ£g π£)) |
36 | 35 | eqeq1d 2735 |
. . . . . . . . 9
β’ (π₯ = π£ β ((π Ξ£g π₯) = (π Ξ£g π€) β (π Ξ£g π£) = (π Ξ£g π€))) |
37 | 36 | rexbidv 3172 |
. . . . . . . 8
β’ (π₯ = π£ β (βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€) β βπ€ β Word πΆ(π Ξ£g π£) = (π Ξ£g π€))) |
38 | 37 | imbi2d 341 |
. . . . . . 7
β’ (π₯ = π£ β ((π· β Fin β βπ€ β Word πΆ(π Ξ£g π₯) = (π Ξ£g π€)) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g π£) = (π Ξ£g π€)))) |
39 | | wrd0 14433 |
. . . . . . . . 9
β’ β
β Word πΆ |
40 | 39 | a1i 11 |
. . . . . . . 8
β’ (π· β Fin β β
β Word πΆ) |
41 | | simpr 486 |
. . . . . . . . . 10
β’ ((π· β Fin β§ π€ = β
) β π€ = β
) |
42 | 41 | oveq2d 7374 |
. . . . . . . . 9
β’ ((π· β Fin β§ π€ = β
) β (π Ξ£g
π€) = (π Ξ£g
β
)) |
43 | 42 | eqeq2d 2744 |
. . . . . . . 8
β’ ((π· β Fin β§ π€ = β
) β ((π Ξ£g
β
) = (π
Ξ£g π€) β (π Ξ£g β
) =
(π
Ξ£g β
))) |
44 | | eqidd 2734 |
. . . . . . . 8
β’ (π· β Fin β (π Ξ£g
β
) = (π
Ξ£g β
)) |
45 | 40, 43, 44 | rspcedvd 3582 |
. . . . . . 7
β’ (π· β Fin β βπ€ β Word πΆ(π Ξ£g β
) =
(π
Ξ£g π€)) |
46 | | ccatcl 14468 |
. . . . . . . . . . . . . 14
β’ ((π£ β Word πΆ β§ π β Word πΆ) β (π£ ++ π) β Word πΆ) |
47 | 46 | ad5ant24 760 |
. . . . . . . . . . . . 13
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π£ ++ π) β Word πΆ) |
48 | | oveq2 7366 |
. . . . . . . . . . . . . . 15
β’ (π€ = (π£ ++ π) β (π Ξ£g π€) = (π Ξ£g (π£ ++ π))) |
49 | 48 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π€ = (π£ ++ π) β ((π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€) β (π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g (π£ ++ π)))) |
50 | 49 | adantl 483 |
. . . . . . . . . . . . 13
β’
(((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β§ π€ = (π£ ++ π)) β ((π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€) β (π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g (π£ ++ π)))) |
51 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π Ξ£g π’) = (π Ξ£g π£)) |
52 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β π· β Fin) |
53 | 52 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π· β Fin) |
54 | 11 | symggrp 19187 |
. . . . . . . . . . . . . . . . . 18
β’ (π· β Fin β π β Grp) |
55 | | grpmnd 18760 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Grp β π β Mnd) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β Mnd) |
57 | 16, 11, 12 | symgtrf 19256 |
. . . . . . . . . . . . . . . . . . 19
β’ ran
(pmTrspβπ·) β
(Baseβπ) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β ran
(pmTrspβπ·) β
(Baseβπ)) |
59 | | simp-5r 785 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β π β ran (pmTrspβπ·)) |
60 | 59 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β ran (pmTrspβπ·)) |
61 | 58, 60 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β (Baseβπ)) |
62 | | simp-6r 787 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β ran (pmTrspβπ·)) |
63 | 58, 62 | sseldd 3946 |
. . . . . . . . . . . . . . . . 17
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β (Baseβπ)) |
64 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’
(+gβπ) = (+gβπ) |
65 | 12, 64 | gsumws2 18657 |
. . . . . . . . . . . . . . . . 17
β’ ((π β Mnd β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π Ξ£g
β¨βππββ©) = (π(+gβπ)π)) |
66 | 56, 61, 63, 65 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π Ξ£g
β¨βππββ©) = (π(+gβπ)π)) |
67 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π(+gβπ)π) = (π Ξ£g π)) |
68 | 66, 67 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π Ξ£g
β¨βππββ©) = (π Ξ£g
π)) |
69 | 51, 68 | oveq12d 7376 |
. . . . . . . . . . . . . 14
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β ((π Ξ£g π’)(+gβπ)(π Ξ£g
β¨βππββ©)) = ((π Ξ£g
π£)(+gβπ)(π Ξ£g π))) |
70 | | sswrd 14416 |
. . . . . . . . . . . . . . . . 17
β’ (ran
(pmTrspβπ·) β
(Baseβπ) β Word
ran (pmTrspβπ·)
β Word (Baseβπ)) |
71 | 58, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β Word ran
(pmTrspβπ·) β
Word (Baseβπ)) |
72 | | simp-7l 788 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π’ β Word ran (pmTrspβπ·)) |
73 | 71, 72 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π’ β Word (Baseβπ)) |
74 | 61, 63 | s2cld 14766 |
. . . . . . . . . . . . . . 15
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β β¨βππββ© β Word (Baseβπ)) |
75 | 12, 64 | gsumccat 18656 |
. . . . . . . . . . . . . . 15
β’ ((π β Mnd β§ π’ β Word (Baseβπ) β§ β¨βππββ© β Word (Baseβπ)) β (π Ξ£g (π’ ++ β¨βππββ©)) = ((π Ξ£g π’)(+gβπ)(π Ξ£g
β¨βππββ©))) |
76 | 56, 73, 74, 75 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π Ξ£g (π’ ++ β¨βππββ©)) = ((π Ξ£g π’)(+gβπ)(π Ξ£g
β¨βππββ©))) |
77 | | cyc3genpm.t |
. . . . . . . . . . . . . . . . . . . 20
β’ πΆ = (π β (β‘β― β {3})) |
78 | | cyc3genpm.m |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (toCycβπ·) |
79 | 78 | imaeq1i 6011 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘β― β {3})) = ((toCycβπ·) β (β‘β― β {3})) |
80 | 77, 79 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . 19
β’ πΆ = ((toCycβπ·) β (β‘β― β {3})) |
81 | 80, 9 | cyc3evpm 32048 |
. . . . . . . . . . . . . . . . . 18
β’ (π· β Fin β πΆ β π΄) |
82 | 11, 12 | evpmss 21006 |
. . . . . . . . . . . . . . . . . . 19
β’
(pmEvenβπ·)
β (Baseβπ) |
83 | 9, 82 | eqsstri 3979 |
. . . . . . . . . . . . . . . . . 18
β’ π΄ β (Baseβπ) |
84 | 81, 83 | sstrdi 3957 |
. . . . . . . . . . . . . . . . 17
β’ (π· β Fin β πΆ β (Baseβπ)) |
85 | | sswrd 14416 |
. . . . . . . . . . . . . . . . 17
β’ (πΆ β (Baseβπ) β Word πΆ β Word (Baseβπ)) |
86 | 53, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β Word πΆ β Word (Baseβπ)) |
87 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π£ β Word πΆ) |
88 | 86, 87 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π£ β Word (Baseβπ)) |
89 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β Word πΆ) |
90 | 86, 89 | sseldd 3946 |
. . . . . . . . . . . . . . 15
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β π β Word (Baseβπ)) |
91 | 12, 64 | gsumccat 18656 |
. . . . . . . . . . . . . . 15
β’ ((π β Mnd β§ π£ β Word (Baseβπ) β§ π β Word (Baseβπ)) β (π Ξ£g (π£ ++ π)) = ((π Ξ£g π£)(+gβπ)(π Ξ£g π))) |
92 | 56, 88, 90, 91 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π Ξ£g (π£ ++ π)) = ((π Ξ£g π£)(+gβπ)(π Ξ£g π))) |
93 | 69, 76, 92 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β (π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g (π£ ++ π))) |
94 | 47, 50, 93 | rspcedvd 3582 |
. . . . . . . . . . . 12
β’
((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β Word πΆ) β§ (π(+gβπ)π) = (π Ξ£g π)) β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€)) |
95 | | cyc3genpm.n |
. . . . . . . . . . . . . . 15
β’ π = (β―βπ·) |
96 | | simp-6r 787 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π β π·) |
97 | | simp-5r 785 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π β π·) |
98 | | simpllr 775 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π β π·) |
99 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β β β π·) |
100 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β (π β π β§ π = (πββ¨βππββ©))) |
101 | 100 | simprd 497 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π = (πββ¨βππββ©)) |
102 | | simprr 772 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π = (πββ¨βπβββ©)) |
103 | 52 | ad6antr 735 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π· β Fin) |
104 | 100 | simpld 496 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π β π) |
105 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β π β β) |
106 | 77, 9, 11, 95, 78, 64, 96, 97, 98, 99, 101, 102, 103, 104, 105 | cyc3genpmlem 32049 |
. . . . . . . . . . . . . 14
β’
((((((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β§ π β π·) β§ β β π·) β§ (π β β β§ π = (πββ¨βπβββ©))) β βπ β Word πΆ(π(+gβπ)π) = (π Ξ£g π)) |
107 | | simp-6r 787 |
. . . . . . . . . . . . . . 15
β’
(((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β π· β Fin) |
108 | | simp-7r 789 |
. . . . . . . . . . . . . . 15
β’
(((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β π β ran (pmTrspβπ·)) |
109 | 16, 78 | trsp2cyc 32021 |
. . . . . . . . . . . . . . 15
β’ ((π· β Fin β§ π β ran (pmTrspβπ·)) β βπ β π· ββ β π· (π β β β§ π = (πββ¨βπβββ©))) |
110 | 107, 108,
109 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β βπ β π· ββ β π· (π β β β§ π = (πββ¨βπβββ©))) |
111 | 106, 110 | r19.29vva 3204 |
. . . . . . . . . . . . 13
β’
(((((((((π’ β
Word ran (pmTrspβπ·)
β§ π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β§ π β π·) β§ π β π·) β§ (π β π β§ π = (πββ¨βππββ©))) β βπ β Word πΆ(π(+gβπ)π) = (π Ξ£g π)) |
112 | 16, 78 | trsp2cyc 32021 |
. . . . . . . . . . . . . 14
β’ ((π· β Fin β§ π β ran (pmTrspβπ·)) β βπ β π· βπ β π· (π β π β§ π = (πββ¨βππββ©))) |
113 | 52, 59, 112 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
((((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β βπ β π· βπ β π· (π β π β§ π = (πββ¨βππββ©))) |
114 | 111, 113 | r19.29vva 3204 |
. . . . . . . . . . . 12
β’
((((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β βπ β Word πΆ(π(+gβπ)π) = (π Ξ£g π)) |
115 | 94, 114 | r19.29a 3156 |
. . . . . . . . . . 11
β’
((((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€)) |
116 | 115 | adantl3r 749 |
. . . . . . . . . 10
β’
(((((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β§ π· β Fin) β§ π£ β Word πΆ) β§ (π Ξ£g π’) = (π Ξ£g π£)) β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€)) |
117 | | simpr 486 |
. . . . . . . . . . . 12
β’
(((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β§ π· β Fin) β π· β Fin) |
118 | | simplr 768 |
. . . . . . . . . . . 12
β’
(((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β§ π· β Fin) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) |
119 | 117, 118 | mpd 15 |
. . . . . . . . . . 11
β’
(((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β§ π· β Fin) β βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€)) |
120 | | oveq2 7366 |
. . . . . . . . . . . . 13
β’ (π£ = π€ β (π Ξ£g π£) = (π Ξ£g π€)) |
121 | 120 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π£ = π€ β ((π Ξ£g π’) = (π Ξ£g π£) β (π Ξ£g π’) = (π Ξ£g π€))) |
122 | 121 | cbvrexvw 3225 |
. . . . . . . . . . 11
β’
(βπ£ β
Word πΆ(π Ξ£g π’) = (π Ξ£g π£) β βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€)) |
123 | 119, 122 | sylibr 233 |
. . . . . . . . . 10
β’
(((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β§ π· β Fin) β βπ£ β Word πΆ(π Ξ£g π’) = (π Ξ£g π£)) |
124 | 116, 123 | r19.29a 3156 |
. . . . . . . . 9
β’
(((((π’ β Word
ran (pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β§ π· β Fin) β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€)) |
125 | 124 | ex 414 |
. . . . . . . 8
β’ ((((π’ β Word ran
(pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β§
π β ran
(pmTrspβπ·)) β§
(π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€))) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€))) |
126 | 125 | ex3 1347 |
. . . . . . 7
β’ ((π’ β Word ran
(pmTrspβπ·) β§
π β ran
(pmTrspβπ·) β§
π β ran
(pmTrspβπ·)) β
((π· β Fin β
βπ€ β Word πΆ(π Ξ£g π’) = (π Ξ£g π€)) β (π· β Fin β βπ€ β Word πΆ(π Ξ£g (π’ ++ β¨βππββ©)) = (π Ξ£g π€)))) |
127 | 26, 30, 34, 38, 45, 126 | wrdt2ind 31856 |
. . . . . 6
β’ ((π£ β Word ran
(pmTrspβπ·) β§ 2
β₯ (β―βπ£))
β (π· β Fin β
βπ€ β Word πΆ(π Ξ£g π£) = (π Ξ£g π€))) |
128 | 127 | imp 408 |
. . . . 5
β’ (((π£ β Word ran
(pmTrspβπ·) β§ 2
β₯ (β―βπ£))
β§ π· β Fin) β
βπ€ β Word πΆ(π Ξ£g π£) = (π Ξ£g π€)) |
129 | 1, 22, 7, 128 | syl21anc 837 |
. . . 4
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β βπ€ β Word πΆ(π Ξ£g π£) = (π Ξ£g π€)) |
130 | 5 | eqeq1d 2735 |
. . . . 5
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β (π = (π Ξ£g π€) β (π Ξ£g π£) = (π Ξ£g π€))) |
131 | 130 | rexbidv 3172 |
. . . 4
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β (βπ€ β Word πΆπ = (π Ξ£g π€) β βπ€ β Word πΆ(π Ξ£g π£) = (π Ξ£g π€))) |
132 | 129, 131 | mpbird 257 |
. . 3
β’ ((((π· β Fin β§ π β π΄) β§ π£ β Word ran (pmTrspβπ·)) β§ π = (π Ξ£g π£)) β βπ€ β Word πΆπ = (π Ξ£g π€)) |
133 | 83 | sseli 3941 |
. . . 4
β’ (π β π΄ β π β (Baseβπ)) |
134 | 11, 12, 16 | psgnfitr 19304 |
. . . . 5
β’ (π· β Fin β (π β (Baseβπ) β βπ£ β Word ran
(pmTrspβπ·)π = (π Ξ£g π£))) |
135 | 134 | biimpa 478 |
. . . 4
β’ ((π· β Fin β§ π β (Baseβπ)) β βπ£ β Word ran
(pmTrspβπ·)π = (π Ξ£g π£)) |
136 | 133, 135 | sylan2 594 |
. . 3
β’ ((π· β Fin β§ π β π΄) β βπ£ β Word ran (pmTrspβπ·)π = (π Ξ£g π£)) |
137 | 132, 136 | r19.29a 3156 |
. 2
β’ ((π· β Fin β§ π β π΄) β βπ€ β Word πΆπ = (π Ξ£g π€)) |
138 | | simpr 486 |
. . . 4
β’ (((π· β Fin β§ π€ β Word πΆ) β§ π = (π Ξ£g π€)) β π = (π Ξ£g π€)) |
139 | 11 | altgnsg 32047 |
. . . . . . . . 9
β’ (π· β Fin β
(pmEvenβπ·) β
(NrmSGrpβπ)) |
140 | 9, 139 | eqeltrid 2838 |
. . . . . . . 8
β’ (π· β Fin β π΄ β (NrmSGrpβπ)) |
141 | | nsgsubg 18965 |
. . . . . . . 8
β’ (π΄ β (NrmSGrpβπ) β π΄ β (SubGrpβπ)) |
142 | | subgsubm 18955 |
. . . . . . . 8
β’ (π΄ β (SubGrpβπ) β π΄ β (SubMndβπ)) |
143 | 140, 141,
142 | 3syl 18 |
. . . . . . 7
β’ (π· β Fin β π΄ β (SubMndβπ)) |
144 | 143 | adantr 482 |
. . . . . 6
β’ ((π· β Fin β§ π€ β Word πΆ) β π΄ β (SubMndβπ)) |
145 | | sswrd 14416 |
. . . . . . . 8
β’ (πΆ β π΄ β Word πΆ β Word π΄) |
146 | 81, 145 | syl 17 |
. . . . . . 7
β’ (π· β Fin β Word πΆ β Word π΄) |
147 | 146 | sselda 3945 |
. . . . . 6
β’ ((π· β Fin β§ π€ β Word πΆ) β π€ β Word π΄) |
148 | | gsumwsubmcl 18652 |
. . . . . 6
β’ ((π΄ β (SubMndβπ) β§ π€ β Word π΄) β (π Ξ£g π€) β π΄) |
149 | 144, 147,
148 | syl2anc 585 |
. . . . 5
β’ ((π· β Fin β§ π€ β Word πΆ) β (π Ξ£g π€) β π΄) |
150 | 149 | adantr 482 |
. . . 4
β’ (((π· β Fin β§ π€ β Word πΆ) β§ π = (π Ξ£g π€)) β (π Ξ£g π€) β π΄) |
151 | 138, 150 | eqeltrd 2834 |
. . 3
β’ (((π· β Fin β§ π€ β Word πΆ) β§ π = (π Ξ£g π€)) β π β π΄) |
152 | 151 | r19.29an 3152 |
. 2
β’ ((π· β Fin β§ βπ€ β Word πΆπ = (π Ξ£g π€)) β π β π΄) |
153 | 137, 152 | impbida 800 |
1
β’ (π· β Fin β (π β π΄ β βπ€ β Word πΆπ = (π Ξ£g π€))) |