Metamath Proof Explorer

Theorem gsmsymgrfix

Description: The composition of permutations fixing one element also fixes this element. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s 
|- S = ( SymGrp ` N )
gsmsymgrfix.b 
|- B = ( Base ` S )
Assertion gsmsymgrfix 
|- ( ( N e. Fin /\ K e. N /\ W e. Word B ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) )

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s 
 |-  S = ( SymGrp ` N )
2 gsmsymgrfix.b 
 |-  B = ( Base ` S )
3 hasheq0 
 |-  ( w e. _V -> ( ( # ` w ) = 0 <-> w = (/) ) )
4 3 elv 
 |-  ( ( # ` w ) = 0 <-> w = (/) )
5 4 biimpri 
 |-  ( w = (/) -> ( # ` w ) = 0 )
6 5 oveq2d 
 |-  ( w = (/) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ 0 ) )
7 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
8 6 7 eqtrdi 
 |-  ( w = (/) -> ( 0 ..^ ( # ` w ) ) = (/) )
9 fveq1 
 |-  ( w = (/) -> ( w ` i ) = ( (/) ` i ) )
10 9 fveq1d 
 |-  ( w = (/) -> ( ( w ` i ) ` K ) = ( ( (/) ` i ) ` K ) )
11 10 eqeq1d 
 |-  ( w = (/) -> ( ( ( w ` i ) ` K ) = K <-> ( ( (/) ` i ) ` K ) = K ) )
12 8 11 raleqbidv 
 |-  ( w = (/) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K <-> A. i e. (/) ( ( (/) ` i ) ` K ) = K ) )
13 oveq2 
 |-  ( w = (/) -> ( S gsum w ) = ( S gsum (/) ) )
14 13 fveq1d 
 |-  ( w = (/) -> ( ( S gsum w ) ` K ) = ( ( S gsum (/) ) ` K ) )
15 14 eqeq1d 
 |-  ( w = (/) -> ( ( ( S gsum w ) ` K ) = K <-> ( ( S gsum (/) ) ` K ) = K ) )
16 12 15 imbi12d 
 |-  ( w = (/) -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) <-> ( A. i e. (/) ( ( (/) ` i ) ` K ) = K -> ( ( S gsum (/) ) ` K ) = K ) ) )
17 16 imbi2d 
 |-  ( w = (/) -> ( ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) ) <-> ( ( N e. Fin /\ K e. N ) -> ( A. i e. (/) ( ( (/) ` i ) ` K ) = K -> ( ( S gsum (/) ) ` K ) = K ) ) ) )
18 fveq2 
 |-  ( w = y -> ( # ` w ) = ( # ` y ) )
19 18 oveq2d 
 |-  ( w = y -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` y ) ) )
20 fveq1 
 |-  ( w = y -> ( w ` i ) = ( y ` i ) )
21 20 fveq1d 
 |-  ( w = y -> ( ( w ` i ) ` K ) = ( ( y ` i ) ` K ) )
22 21 eqeq1d 
 |-  ( w = y -> ( ( ( w ` i ) ` K ) = K <-> ( ( y ` i ) ` K ) = K ) )
23 19 22 raleqbidv 
 |-  ( w = y -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K ) )
24 oveq2 
 |-  ( w = y -> ( S gsum w ) = ( S gsum y ) )
25 24 fveq1d 
 |-  ( w = y -> ( ( S gsum w ) ` K ) = ( ( S gsum y ) ` K ) )
26 25 eqeq1d 
 |-  ( w = y -> ( ( ( S gsum w ) ` K ) = K <-> ( ( S gsum y ) ` K ) = K ) )
27 23 26 imbi12d 
 |-  ( w = y -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) <-> ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) )
28 27 imbi2d 
 |-  ( w = y -> ( ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) ) <-> ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) ) )
29 fveq2 
 |-  ( w = ( y ++ <" z "> ) -> ( # ` w ) = ( # ` ( y ++ <" z "> ) ) )
30 29 oveq2d 
 |-  ( w = ( y ++ <" z "> ) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) )
31 fveq1 
 |-  ( w = ( y ++ <" z "> ) -> ( w ` i ) = ( ( y ++ <" z "> ) ` i ) )
32 31 fveq1d 
 |-  ( w = ( y ++ <" z "> ) -> ( ( w ` i ) ` K ) = ( ( ( y ++ <" z "> ) ` i ) ` K ) )
33 32 eqeq1d 
 |-  ( w = ( y ++ <" z "> ) -> ( ( ( w ` i ) ` K ) = K <-> ( ( ( y ++ <" z "> ) ` i ) ` K ) = K ) )
34 30 33 raleqbidv 
 |-  ( w = ( y ++ <" z "> ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K ) )
35 oveq2 
 |-  ( w = ( y ++ <" z "> ) -> ( S gsum w ) = ( S gsum ( y ++ <" z "> ) ) )
36 35 fveq1d 
 |-  ( w = ( y ++ <" z "> ) -> ( ( S gsum w ) ` K ) = ( ( S gsum ( y ++ <" z "> ) ) ` K ) )
37 36 eqeq1d 
 |-  ( w = ( y ++ <" z "> ) -> ( ( ( S gsum w ) ` K ) = K <-> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) )
38 34 37 imbi12d 
 |-  ( w = ( y ++ <" z "> ) -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) <-> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) ) )
39 38 imbi2d 
 |-  ( w = ( y ++ <" z "> ) -> ( ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) ) <-> ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) ) ) )
40 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
41 40 oveq2d 
 |-  ( w = W -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` W ) ) )
42 fveq1 
 |-  ( w = W -> ( w ` i ) = ( W ` i ) )
43 42 fveq1d 
 |-  ( w = W -> ( ( w ` i ) ` K ) = ( ( W ` i ) ` K ) )
44 43 eqeq1d 
 |-  ( w = W -> ( ( ( w ` i ) ` K ) = K <-> ( ( W ` i ) ` K ) = K ) )
45 41 44 raleqbidv 
 |-  ( w = W -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K ) )
46 oveq2 
 |-  ( w = W -> ( S gsum w ) = ( S gsum W ) )
47 46 fveq1d 
 |-  ( w = W -> ( ( S gsum w ) ` K ) = ( ( S gsum W ) ` K ) )
48 47 eqeq1d 
 |-  ( w = W -> ( ( ( S gsum w ) ` K ) = K <-> ( ( S gsum W ) ` K ) = K ) )
49 45 48 imbi12d 
 |-  ( w = W -> ( ( 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 ) ) )
50 49 imbi2d 
 |-  ( w = W -> ( ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) ( ( w ` i ) ` K ) = K -> ( ( S gsum w ) ` K ) = K ) ) <-> ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) ) )
51 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
52 51 gsum0 
 |-  ( S gsum (/) ) = ( 0g ` S )
53 1 symgid 
 |-  ( N e. Fin -> ( _I |` N ) = ( 0g ` S ) )
54 53 adantr 
 |-  ( ( N e. Fin /\ K e. N ) -> ( _I |` N ) = ( 0g ` S ) )
55 52 54 eqtr4id 
 |-  ( ( N e. Fin /\ K e. N ) -> ( S gsum (/) ) = ( _I |` N ) )
56 55 fveq1d 
 |-  ( ( N e. Fin /\ K e. N ) -> ( ( S gsum (/) ) ` K ) = ( ( _I |` N ) ` K ) )
57 fvresi 
 |-  ( K e. N -> ( ( _I |` N ) ` K ) = K )
58 57 adantl 
 |-  ( ( N e. Fin /\ K e. N ) -> ( ( _I |` N ) ` K ) = K )
59 56 58 eqtrd 
 |-  ( ( N e. Fin /\ K e. N ) -> ( ( S gsum (/) ) ` K ) = K )
60 59 a1d 
 |-  ( ( N e. Fin /\ K e. N ) -> ( A. i e. (/) ( ( (/) ` i ) ` K ) = K -> ( ( S gsum (/) ) ` K ) = K ) )
61 ccatws1len 
 |-  ( y e. Word B -> ( # ` ( y ++ <" z "> ) ) = ( ( # ` y ) + 1 ) )
62 61 oveq2d 
 |-  ( y e. Word B -> ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) = ( 0 ..^ ( ( # ` y ) + 1 ) ) )
63 62 raleqdv 
 |-  ( y e. Word B -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( ( # ` y ) + 1 ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K ) )
64 63 adantr 
 |-  ( ( y e. Word B /\ z e. B ) -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( ( # ` y ) + 1 ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K ) )
65 64 adantr 
 |-  ( ( ( y e. Word B /\ z e. B ) /\ ( ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) ) -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K <-> A. i e. ( 0 ..^ ( ( # ` y ) + 1 ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K ) )
66 1 2 gsmsymgrfixlem1 
 |-  ( ( ( y e. Word B /\ z e. B ) /\ ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) -> ( A. i e. ( 0 ..^ ( ( # ` y ) + 1 ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) )
67 66 3expb 
 |-  ( ( ( y e. Word B /\ z e. B ) /\ ( ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` y ) + 1 ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) )
68 65 67 sylbid 
 |-  ( ( ( y e. Word B /\ z e. B ) /\ ( ( N e. Fin /\ K e. N ) /\ ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) ) -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) )
69 68 exp32 
 |-  ( ( y e. Word B /\ z e. B ) -> ( ( N e. Fin /\ K e. N ) -> ( ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) ) ) )
70 69 a2d 
 |-  ( ( y e. Word B /\ z e. B ) -> ( ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` y ) ) ( ( y ` i ) ` K ) = K -> ( ( S gsum y ) ` K ) = K ) ) -> ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` ( y ++ <" z "> ) ) ) ( ( ( y ++ <" z "> ) ` i ) ` K ) = K -> ( ( S gsum ( y ++ <" z "> ) ) ` K ) = K ) ) ) )
71 17 28 39 50 60 70 wrdind 
 |-  ( W e. Word B -> ( ( N e. Fin /\ K e. N ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) )
72 71 com12 
 |-  ( ( N e. Fin /\ K e. N ) -> ( W e. Word B -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) ) )
73 72 3impia 
 |-  ( ( N e. Fin /\ K e. N /\ W e. Word B ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) ( ( W ` i ) ` K ) = K -> ( ( S gsum W ) ` K ) = K ) )