# 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 ..^ ( # ` (/) ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 "> ) ) ) )`
` |-  ( ( 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 syl6bb
` |-  ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) ) )`