Metamath Proof Explorer

Theorem gsmsymgreq

Description: Two combination of permutations moves an element of the intersection of the base sets of the permutations to the same element if each pair of corresponding permutations moves such an element to the same element. (Contributed by AV, 20-Jan-2019)

Ref Expression
Hypotheses gsmsymgrfix.s 
|- S = ( SymGrp ` N )
gsmsymgrfix.b 
|- B = ( Base ` S )
gsmsymgreq.z 
|- Z = ( SymGrp ` M )
gsmsymgreq.p 
|- P = ( Base ` Z )
gsmsymgreq.i 
|- I = ( N i^i M )
Assertion gsmsymgreq 
|- ( ( ( N e. Fin /\ M e. Fin ) /\ ( W e. Word B /\ U e. Word P /\ ( # ` W ) = ( # ` U ) ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) )

Proof

Step Hyp Ref Expression
1 gsmsymgrfix.s 
 |-  S = ( SymGrp ` N )
2 gsmsymgrfix.b 
 |-  B = ( Base ` S )
3 gsmsymgreq.z 
 |-  Z = ( SymGrp ` M )
4 gsmsymgreq.p 
 |-  P = ( Base ` Z )
5 gsmsymgreq.i 
 |-  I = ( N i^i M )
6 fveq2 
 |-  ( w = (/) -> ( # ` w ) = ( # ` (/) ) )
7 6 oveq2d 
 |-  ( w = (/) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` (/) ) ) )
8 7 adantr 
 |-  ( ( w = (/) /\ u = (/) ) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` (/) ) ) )
9 fveq1 
 |-  ( w = (/) -> ( w ` i ) = ( (/) ` i ) )
10 9 fveq1d 
 |-  ( w = (/) -> ( ( w ` i ) ` n ) = ( ( (/) ` i ) ` n ) )
11 fveq1 
 |-  ( u = (/) -> ( u ` i ) = ( (/) ` i ) )
12 11 fveq1d 
 |-  ( u = (/) -> ( ( u ` i ) ` n ) = ( ( (/) ` i ) ` n ) )
13 10 12 eqeqan12d 
 |-  ( ( w = (/) /\ u = (/) ) -> ( ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> ( ( (/) ` i ) ` n ) = ( ( (/) ` i ) ` n ) ) )
14 13 ralbidv 
 |-  ( ( w = (/) /\ u = (/) ) -> ( A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. n e. I ( ( (/) ` i ) ` n ) = ( ( (/) ` i ) ` n ) ) )
15 8 14 raleqbidv 
 |-  ( ( w = (/) /\ u = (/) ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. i e. ( 0 ..^ ( # ` (/) ) ) A. n e. I ( ( (/) ` i ) ` n ) = ( ( (/) ` i ) ` n ) ) )
16 oveq2 
 |-  ( w = (/) -> ( S gsum w ) = ( S gsum (/) ) )
17 16 fveq1d 
 |-  ( w = (/) -> ( ( S gsum w ) ` n ) = ( ( S gsum (/) ) ` n ) )
18 oveq2 
 |-  ( u = (/) -> ( Z gsum u ) = ( Z gsum (/) ) )
19 18 fveq1d 
 |-  ( u = (/) -> ( ( Z gsum u ) ` n ) = ( ( Z gsum (/) ) ` n ) )
20 17 19 eqeqan12d 
 |-  ( ( w = (/) /\ u = (/) ) -> ( ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) ) )
21 20 ralbidv 
 |-  ( ( w = (/) /\ u = (/) ) -> ( A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> A. n e. I ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) ) )
22 15 21 imbi12d 
 |-  ( ( w = (/) /\ u = (/) ) -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) <-> ( A. i e. ( 0 ..^ ( # ` (/) ) ) A. n e. I ( ( (/) ` i ) ` n ) = ( ( (/) ` i ) ` n ) -> A. n e. I ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) ) ) )
23 22 imbi2d 
 |-  ( ( w = (/) /\ u = (/) ) -> ( ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) ) <-> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` (/) ) ) A. n e. I ( ( (/) ` i ) ` n ) = ( ( (/) ` i ) ` n ) -> A. n e. I ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) ) ) ) )
24 fveq2 
 |-  ( w = x -> ( # ` w ) = ( # ` x ) )
25 24 oveq2d 
 |-  ( w = x -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` x ) ) )
26 25 adantr 
 |-  ( ( w = x /\ u = y ) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` x ) ) )
27 fveq1 
 |-  ( w = x -> ( w ` i ) = ( x ` i ) )
28 27 fveq1d 
 |-  ( w = x -> ( ( w ` i ) ` n ) = ( ( x ` i ) ` n ) )
29 fveq1 
 |-  ( u = y -> ( u ` i ) = ( y ` i ) )
30 29 fveq1d 
 |-  ( u = y -> ( ( u ` i ) ` n ) = ( ( y ` i ) ` n ) )
31 28 30 eqeqan12d 
 |-  ( ( w = x /\ u = y ) -> ( ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) ) )
32 31 ralbidv 
 |-  ( ( w = x /\ u = y ) -> ( A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) ) )
33 26 32 raleqbidv 
 |-  ( ( w = x /\ u = y ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. i e. ( 0 ..^ ( # ` x ) ) A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) ) )
34 oveq2 
 |-  ( w = x -> ( S gsum w ) = ( S gsum x ) )
35 34 fveq1d 
 |-  ( w = x -> ( ( S gsum w ) ` n ) = ( ( S gsum x ) ` n ) )
36 oveq2 
 |-  ( u = y -> ( Z gsum u ) = ( Z gsum y ) )
37 36 fveq1d 
 |-  ( u = y -> ( ( Z gsum u ) ` n ) = ( ( Z gsum y ) ` n ) )
38 35 37 eqeqan12d 
 |-  ( ( w = x /\ u = y ) -> ( ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) )
39 38 ralbidv 
 |-  ( ( w = x /\ u = y ) -> ( A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> A. n e. I ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) )
40 33 39 imbi12d 
 |-  ( ( w = x /\ u = y ) -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) <-> ( A. i e. ( 0 ..^ ( # ` x ) ) A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) -> A. n e. I ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) ) )
41 40 imbi2d 
 |-  ( ( w = x /\ u = y ) -> ( ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) ) <-> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` x ) ) A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) -> A. n e. I ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) ) ) )
42 fveq2 
 |-  ( w = ( x ++ <" b "> ) -> ( # ` w ) = ( # ` ( x ++ <" b "> ) ) )
43 42 oveq2d 
 |-  ( w = ( x ++ <" b "> ) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) )
44 43 adantr 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) )
45 fveq1 
 |-  ( w = ( x ++ <" b "> ) -> ( w ` i ) = ( ( x ++ <" b "> ) ` i ) )
46 45 fveq1d 
 |-  ( w = ( x ++ <" b "> ) -> ( ( w ` i ) ` n ) = ( ( ( x ++ <" b "> ) ` i ) ` n ) )
47 fveq1 
 |-  ( u = ( y ++ <" p "> ) -> ( u ` i ) = ( ( y ++ <" p "> ) ` i ) )
48 47 fveq1d 
 |-  ( u = ( y ++ <" p "> ) -> ( ( u ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) )
49 46 48 eqeqan12d 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) ) )
50 49 ralbidv 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) ) )
51 44 50 raleqbidv 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. i e. ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) ) )
52 oveq2 
 |-  ( w = ( x ++ <" b "> ) -> ( S gsum w ) = ( S gsum ( x ++ <" b "> ) ) )
53 52 fveq1d 
 |-  ( w = ( x ++ <" b "> ) -> ( ( S gsum w ) ` n ) = ( ( S gsum ( x ++ <" b "> ) ) ` n ) )
54 oveq2 
 |-  ( u = ( y ++ <" p "> ) -> ( Z gsum u ) = ( Z gsum ( y ++ <" p "> ) ) )
55 54 fveq1d 
 |-  ( u = ( y ++ <" p "> ) -> ( ( Z gsum u ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) )
56 53 55 eqeqan12d 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) )
57 56 ralbidv 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> A. n e. I ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) )
58 51 57 imbi12d 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) <-> ( A. i e. ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) ) )
59 58 imbi2d 
 |-  ( ( w = ( x ++ <" b "> ) /\ u = ( y ++ <" p "> ) ) -> ( ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) ) <-> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) ) ) )
60 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
61 60 oveq2d 
 |-  ( w = W -> ( 0 ..^ ( # ` w ) ) = ( 0 ..^ ( # ` W ) ) )
62 fveq1 
 |-  ( w = W -> ( w ` i ) = ( W ` i ) )
63 62 fveq1d 
 |-  ( w = W -> ( ( w ` i ) ` n ) = ( ( W ` i ) ` n ) )
64 63 eqeq1d 
 |-  ( w = W -> ( ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) <-> ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) )
65 64 ralbidv 
 |-  ( w = W -> ( A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) <-> A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) )
66 61 65 raleqbidv 
 |-  ( w = W -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) <-> A. i e. ( 0 ..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) ) )
67 oveq2 
 |-  ( w = W -> ( S gsum w ) = ( S gsum W ) )
68 67 fveq1d 
 |-  ( w = W -> ( ( S gsum w ) ` n ) = ( ( S gsum W ) ` n ) )
69 68 eqeq1d 
 |-  ( w = W -> ( ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) <-> ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) )
70 69 ralbidv 
 |-  ( w = W -> ( A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) <-> A. n e. I ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) )
71 66 70 imbi12d 
 |-  ( w = W -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) ) <-> ( A. i e. ( 0 ..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) ) )
72 71 imbi2d 
 |-  ( w = W -> ( ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) ) ) <-> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) ) ) )
73 fveq1 
 |-  ( u = U -> ( u ` i ) = ( U ` i ) )
74 73 fveq1d 
 |-  ( u = U -> ( ( u ` i ) ` n ) = ( ( U ` i ) ` n ) )
75 74 eqeq2d 
 |-  ( u = U -> ( ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) ) )
76 75 ralbidv 
 |-  ( u = U -> ( A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) ) )
77 76 ralbidv 
 |-  ( u = U -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) <-> A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) ) )
78 oveq2 
 |-  ( u = U -> ( Z gsum u ) = ( Z gsum U ) )
79 78 fveq1d 
 |-  ( u = U -> ( ( Z gsum u ) ` n ) = ( ( Z gsum U ) ` n ) )
80 79 eqeq2d 
 |-  ( u = U -> ( ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) ) )
81 80 ralbidv 
 |-  ( u = U -> ( A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) <-> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) ) )
82 77 81 imbi12d 
 |-  ( u = U -> ( ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) <-> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) ) ) )
83 82 imbi2d 
 |-  ( u = U -> ( ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( u ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum u ) ` n ) ) ) <-> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` w ) ) A. n e. I ( ( w ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum w ) ` n ) = ( ( Z gsum U ) ` n ) ) ) ) )
84 eleq2 
 |-  ( I = ( N i^i M ) -> ( n e. I <-> n e. ( N i^i M ) ) )
85 elin 
 |-  ( n e. ( N i^i M ) <-> ( n e. N /\ n e. M ) )
86 84 85 bitrdi 
 |-  ( I = ( N i^i M ) -> ( n e. I <-> ( n e. N /\ n e. M ) ) )
87 simpl 
 |-  ( ( n e. N /\ n e. M ) -> n e. N )
88 86 87 syl6bi 
 |-  ( I = ( N i^i M ) -> ( n e. I -> n e. N ) )
89 5 88 ax-mp 
 |-  ( n e. I -> n e. N )
90 89 adantl 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ n e. I ) -> n e. N )
91 fvresi 
 |-  ( n e. N -> ( ( _I |` N ) ` n ) = n )
92 90 91 syl 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ n e. I ) -> ( ( _I |` N ) ` n ) = n )
93 simpr 
 |-  ( ( n e. N /\ n e. M ) -> n e. M )
94 86 93 syl6bi 
 |-  ( I = ( N i^i M ) -> ( n e. I -> n e. M ) )
95 5 94 ax-mp 
 |-  ( n e. I -> n e. M )
96 95 adantl 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ n e. I ) -> n e. M )
97 fvresi 
 |-  ( n e. M -> ( ( _I |` M ) ` n ) = n )
98 96 97 syl 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ n e. I ) -> ( ( _I |` M ) ` n ) = n )
99 92 98 eqtr4d 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ n e. I ) -> ( ( _I |` N ) ` n ) = ( ( _I |` M ) ` n ) )
100 99 ralrimiva 
 |-  ( ( N e. Fin /\ M e. Fin ) -> A. n e. I ( ( _I |` N ) ` n ) = ( ( _I |` M ) ` n ) )
101 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
102 101 gsum0 
 |-  ( S gsum (/) ) = ( 0g ` S )
103 1 symgid 
 |-  ( N e. Fin -> ( _I |` N ) = ( 0g ` S ) )
104 103 adantr 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( _I |` N ) = ( 0g ` S ) )
105 102 104 eqtr4id 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( S gsum (/) ) = ( _I |` N ) )
106 105 fveq1d 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( ( S gsum (/) ) ` n ) = ( ( _I |` N ) ` n ) )
107 eqid 
 |-  ( 0g ` Z ) = ( 0g ` Z )
108 107 gsum0 
 |-  ( Z gsum (/) ) = ( 0g ` Z )
109 3 symgid 
 |-  ( M e. Fin -> ( _I |` M ) = ( 0g ` Z ) )
110 109 adantl 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( _I |` M ) = ( 0g ` Z ) )
111 108 110 eqtr4id 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( Z gsum (/) ) = ( _I |` M ) )
112 111 fveq1d 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( ( Z gsum (/) ) ` n ) = ( ( _I |` M ) ` n ) )
113 106 112 eqeq12d 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) <-> ( ( _I |` N ) ` n ) = ( ( _I |` M ) ` n ) ) )
114 113 ralbidv 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( A. n e. I ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) <-> A. n e. I ( ( _I |` N ) ` n ) = ( ( _I |` M ) ` n ) ) )
115 100 114 mpbird 
 |-  ( ( N e. Fin /\ M e. Fin ) -> A. n e. I ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) )
116 115 a1d 
 |-  ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` (/) ) ) A. n e. I ( ( (/) ` i ) ` n ) = ( ( (/) ` i ) ` n ) -> A. n e. I ( ( S gsum (/) ) ` n ) = ( ( Z gsum (/) ) ` n ) ) )
117 1 2 3 4 5 gsmsymgreqlem2 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( x e. Word B /\ b e. B ) /\ ( y e. Word P /\ p e. P ) /\ ( # ` x ) = ( # ` y ) ) ) -> ( ( A. i e. ( 0 ..^ ( # ` x ) ) A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) -> A. n e. I ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) -> ( A. i e. ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) ) )
118 117 expcom 
 |-  ( ( ( x e. Word B /\ b e. B ) /\ ( y e. Word P /\ p e. P ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( N e. Fin /\ M e. Fin ) -> ( ( A. i e. ( 0 ..^ ( # ` x ) ) A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) -> A. n e. I ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) -> ( A. i e. ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) ) ) )
119 118 a2d 
 |-  ( ( ( x e. Word B /\ b e. B ) /\ ( y e. Word P /\ p e. P ) /\ ( # ` x ) = ( # ` y ) ) -> ( ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` x ) ) A. n e. I ( ( x ` i ) ` n ) = ( ( y ` i ) ` n ) -> A. n e. I ( ( S gsum x ) ` n ) = ( ( Z gsum y ) ` n ) ) ) -> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` ( x ++ <" b "> ) ) ) A. n e. I ( ( ( x ++ <" b "> ) ` i ) ` n ) = ( ( ( y ++ <" p "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( x ++ <" b "> ) ) ` n ) = ( ( Z gsum ( y ++ <" p "> ) ) ` n ) ) ) ) )
120 23 41 59 72 83 116 119 wrd2ind 
 |-  ( ( W e. Word B /\ U e. Word P /\ ( # ` W ) = ( # ` U ) ) -> ( ( N e. Fin /\ M e. Fin ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) ) )
121 120 impcom 
 |-  ( ( ( N e. Fin /\ M e. Fin ) /\ ( W e. Word B /\ U e. Word P /\ ( # ` W ) = ( # ` U ) ) ) -> ( A. i e. ( 0 ..^ ( # ` W ) ) A. n e. I ( ( W ` i ) ` n ) = ( ( U ` i ) ` n ) -> A. n e. I ( ( S gsum W ) ` n ) = ( ( Z gsum U ) ` n ) ) )