Step |
Hyp |
Ref |
Expression |
1 |
|
gsmsymgrfix.s |
|- S = ( SymGrp ` N ) |
2 |
|
gsmsymgrfix.b |
|- B = ( Base ` S ) |
3 |
|
lencl |
|- ( W e. Word B -> ( # ` W ) e. NN0 ) |
4 |
|
elnn0uz |
|- ( ( # ` W ) e. NN0 <-> ( # ` W ) e. ( ZZ>= ` 0 ) ) |
5 |
3 4
|
sylib |
|- ( W e. Word B -> ( # ` W ) e. ( ZZ>= ` 0 ) ) |
6 |
5
|
adantr |
|- ( ( W e. Word B /\ P e. B ) -> ( # ` W ) e. ( ZZ>= ` 0 ) ) |
7 |
6
|
3ad2ant1 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( # ` W ) e. ( ZZ>= ` 0 ) ) |
8 |
|
fzosplitsn |
|- ( ( # ` W ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( # ` W ) + 1 ) ) = ( ( 0 ..^ ( # ` W ) ) u. { ( # ` W ) } ) ) |
9 |
7 8
|
syl |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( 0 ..^ ( ( # ` W ) + 1 ) ) = ( ( 0 ..^ ( # ` W ) ) u. { ( # ` W ) } ) ) |
10 |
9
|
raleqdv |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) + 1 ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> A. i e. ( ( 0 ..^ ( # ` W ) ) u. { ( # ` W ) } ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) |
11 |
3
|
adantr |
|- ( ( W e. Word B /\ P e. B ) -> ( # ` W ) e. NN0 ) |
12 |
11
|
3ad2ant1 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( # ` W ) e. NN0 ) |
13 |
|
fveq2 |
|- ( i = ( # ` W ) -> ( ( W ++ <" P "> ) ` i ) = ( ( W ++ <" P "> ) ` ( # ` W ) ) ) |
14 |
13
|
fveq1d |
|- ( i = ( # ` W ) -> ( ( ( W ++ <" P "> ) ` i ) ` K ) = ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) ) |
15 |
14
|
eqeq1d |
|- ( i = ( # ` W ) -> ( ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K ) ) |
16 |
15
|
ralunsn |
|- ( ( # ` W ) e. NN0 -> ( A. i e. ( ( 0 ..^ ( # ` W ) ) u. { ( # ` W ) } ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K /\ ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K ) ) ) |
17 |
12 16
|
syl |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( A. i e. ( ( 0 ..^ ( # ` W ) ) u. { ( # ` W ) } ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K /\ ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K ) ) ) |
18 |
10 17
|
bitrd |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) + 1 ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K /\ ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K ) ) ) |
19 |
|
eqidd |
|- ( ( W e. Word B /\ P e. B ) -> ( # ` W ) = ( # ` W ) ) |
20 |
|
ccats1val2 |
|- ( ( W e. Word B /\ P e. B /\ ( # ` W ) = ( # ` W ) ) -> ( ( W ++ <" P "> ) ` ( # ` W ) ) = P ) |
21 |
20
|
fveq1d |
|- ( ( W e. Word B /\ P e. B /\ ( # ` W ) = ( # ` W ) ) -> ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = ( P ` K ) ) |
22 |
21
|
eqeq1d |
|- ( ( W e. Word B /\ P e. B /\ ( # ` W ) = ( # ` W ) ) -> ( ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K <-> ( P ` K ) = K ) ) |
23 |
19 22
|
mpd3an3 |
|- ( ( W e. Word B /\ P e. B ) -> ( ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K <-> ( P ` K ) = K ) ) |
24 |
23
|
3ad2ant1 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K <-> ( P ` K ) = K ) ) |
25 |
|
simprl |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> N e. Fin ) |
26 |
|
simpll |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> W e. Word B ) |
27 |
|
simplr |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> P e. B ) |
28 |
1 2
|
gsumccatsymgsn |
|- ( ( N e. Fin /\ W e. Word B /\ P e. B ) -> ( S gsum ( W ++ <" P "> ) ) = ( ( S gsum W ) o. P ) ) |
29 |
28
|
fveq1d |
|- ( ( N e. Fin /\ W e. Word B /\ P e. B ) -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = ( ( ( S gsum W ) o. P ) ` K ) ) |
30 |
25 26 27 29
|
syl3anc |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = ( ( ( S gsum W ) o. P ) ` K ) ) |
31 |
30
|
3adant3 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = ( ( ( S gsum W ) o. P ) ` K ) ) |
32 |
31
|
adantr |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) /\ ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = ( ( ( S gsum W ) o. P ) ` K ) ) |
33 |
1 2
|
symgbasf |
|- ( P e. B -> P : N --> N ) |
34 |
33
|
ffnd |
|- ( P e. B -> P Fn N ) |
35 |
34
|
adantl |
|- ( ( W e. Word B /\ P e. B ) -> P Fn N ) |
36 |
|
simpr |
|- ( ( N e. Fin /\ K e. N ) -> K e. N ) |
37 |
|
fvco2 |
|- ( ( P Fn N /\ K e. N ) -> ( ( ( S gsum W ) o. P ) ` K ) = ( ( S gsum W ) ` ( P ` K ) ) ) |
38 |
35 36 37
|
syl2an |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> ( ( ( S gsum W ) o. P ) ` K ) = ( ( S gsum W ) ` ( P ` K ) ) ) |
39 |
38
|
3adant3 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( ( S gsum W ) o. P ) ` K ) = ( ( S gsum W ) ` ( P ` K ) ) ) |
40 |
39
|
adantr |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) /\ ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) -> ( ( ( S gsum W ) o. P ) ` K ) = ( ( S gsum W ) ` ( P ` K ) ) ) |
41 |
|
fveq2 |
|- ( ( P ` K ) = K -> ( ( S gsum W ) ` ( P ` K ) ) = ( ( S gsum W ) ` K ) ) |
42 |
41
|
ad2antrl |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) /\ ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) -> ( ( S gsum W ) ` ( P ` K ) ) = ( ( S gsum W ) ` K ) ) |
43 |
|
ccats1val1 |
|- ( ( W e. Word B /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" P "> ) ` i ) = ( W ` i ) ) |
44 |
43
|
ad4ant14 |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" P "> ) ` i ) = ( W ` i ) ) |
45 |
44
|
fveq1d |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( W ++ <" P "> ) ` i ) ` K ) = ( ( W ` i ) ` K ) ) |
46 |
45
|
eqeq1d |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) /\ i e. ( 0 ..^ ( # ` W ) ) ) -> ( ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> ( ( W ` i ) ` K ) = K ) ) |
47 |
46
|
ralbidva |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K ) ) |
48 |
47
|
biimpd |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K ) ) |
49 |
48
|
adantld |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) ) -> ( ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K ) ) |
50 |
49
|
3adant3 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) -> A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K ) ) |
51 |
|
simp3 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) |
52 |
50 51
|
syld |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) -> ( ( S gsum W ) ` K ) = K ) ) |
53 |
52
|
imp |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) /\ ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) -> ( ( S gsum W ) ` K ) = K ) |
54 |
42 53
|
eqtrd |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) /\ ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) -> ( ( S gsum W ) ` ( P ` K ) ) = K ) |
55 |
32 40 54
|
3eqtrd |
|- ( ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) /\ ( ( P ` K ) = K /\ A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K ) ) -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = K ) |
56 |
55
|
exp32 |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( P ` K ) = K -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = K ) ) ) |
57 |
24 56
|
sylbid |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = K ) ) ) |
58 |
57
|
impcomd |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K /\ ( ( ( W ++ <" P "> ) ` ( # ` W ) ) ` K ) = K ) -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = K ) ) |
59 |
18 58
|
sylbid |
|- ( ( ( W e. Word B /\ P e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) + 1 ) ) ( ( ( W ++ <" P "> ) ` i ) ` K ) = K -> ( ( S gsum ( W ++ <" P "> ) ) ` K ) = K ) ) |