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