Metamath Proof Explorer


Theorem gsmsymgrfixlem1

Description: Lemma 1 for gsmsymgrfix . (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s
|- S = ( SymGrp ` N )
gsmsymgrfix.b
|- B = ( Base ` S )
Assertion gsmsymgrfixlem1
|- ( ( ( 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 ) )

Proof

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 ) )