# Metamath Proof Explorer

## Theorem gsmsymgreqlem2

Description: Lemma 2 for gsmsymgreq . (Contributed by AV, 26-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 gsmsymgreqlem2
`|- ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R 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 ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` 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 ccatws1len
` |-  ( X e. Word B -> ( # ` ( X ++ <" C "> ) ) = ( ( # ` X ) + 1 ) )`
7 6 oveq2d
` |-  ( X e. Word B -> ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) = ( 0 ..^ ( ( # ` X ) + 1 ) ) )`
8 lencl
` |-  ( X e. Word B -> ( # ` X ) e. NN0 )`
9 elnn0uz
` |-  ( ( # ` X ) e. NN0 <-> ( # ` X ) e. ( ZZ>= ` 0 ) )`
10 8 9 sylib
` |-  ( X e. Word B -> ( # ` X ) e. ( ZZ>= ` 0 ) )`
11 fzosplitsn
` |-  ( ( # ` X ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( # ` X ) + 1 ) ) = ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) )`
12 10 11 syl
` |-  ( X e. Word B -> ( 0 ..^ ( ( # ` X ) + 1 ) ) = ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) )`
13 7 12 eqtrd
` |-  ( X e. Word B -> ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) = ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) )`
` |-  ( ( X e. Word B /\ C e. B ) -> ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) = ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) )`
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) = ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) )`
16 15 raleqdv
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( A. i e. ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> A. i e. ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) ) )`
` |-  ( ( X e. Word B /\ C e. B ) -> ( # ` X ) e. NN0 )`
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( # ` X ) e. NN0 )`
19 fveq2
` |-  ( i = ( # ` X ) -> ( ( X ++ <" C "> ) ` i ) = ( ( X ++ <" C "> ) ` ( # ` X ) ) )`
20 19 fveq1d
` |-  ( i = ( # ` X ) -> ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) )`
21 fveq2
` |-  ( i = ( # ` X ) -> ( ( Y ++ <" R "> ) ` i ) = ( ( Y ++ <" R "> ) ` ( # ` X ) ) )`
22 21 fveq1d
` |-  ( i = ( # ` X ) -> ( ( ( Y ++ <" R "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) )`
23 20 22 eqeq12d
` |-  ( i = ( # ` X ) -> ( ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) ) )`
24 23 ralbidv
` |-  ( i = ( # ` X ) -> ( A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> A. n e. I ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) ) )`
25 24 ralunsn
` |-  ( ( # ` X ) e. NN0 -> ( A. i e. ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) /\ A. n e. I ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) ) ) )`
26 18 25 syl
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( A. i e. ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) /\ A. n e. I ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) ) ) )`
27 simp1l
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> X e. Word B )`
28 ccats1val1
` |-  ( ( X e. Word B /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( ( X ++ <" C "> ) ` i ) = ( X ` i ) )`
29 27 28 sylan
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( ( X ++ <" C "> ) ` i ) = ( X ` i ) )`
30 29 fveq1d
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( X ` i ) ` n ) )`
31 simp2l
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> Y e. Word P )`
32 oveq2
` |-  ( ( # ` X ) = ( # ` Y ) -> ( 0 ..^ ( # ` X ) ) = ( 0 ..^ ( # ` Y ) ) )`
33 32 eleq2d
` |-  ( ( # ` X ) = ( # ` Y ) -> ( i e. ( 0 ..^ ( # ` X ) ) <-> i e. ( 0 ..^ ( # ` Y ) ) ) )`
34 33 biimpd
` |-  ( ( # ` X ) = ( # ` Y ) -> ( i e. ( 0 ..^ ( # ` X ) ) -> i e. ( 0 ..^ ( # ` Y ) ) ) )`
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( i e. ( 0 ..^ ( # ` X ) ) -> i e. ( 0 ..^ ( # ` Y ) ) ) )`
36 35 imp
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> i e. ( 0 ..^ ( # ` Y ) ) )`
37 ccats1val1
` |-  ( ( Y e. Word P /\ i e. ( 0 ..^ ( # ` Y ) ) ) -> ( ( Y ++ <" R "> ) ` i ) = ( Y ` i ) )`
38 31 36 37 syl2an2r
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( ( Y ++ <" R "> ) ` i ) = ( Y ` i ) )`
39 38 fveq1d
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( ( ( Y ++ <" R "> ) ` i ) ` n ) = ( ( Y ` i ) ` n ) )`
40 30 39 eqeq12d
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) ) )`
41 40 ralbidv
` |-  ( ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) /\ i e. ( 0 ..^ ( # ` X ) ) ) -> ( A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) ) )`
42 41 ralbidva
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) ) )`
43 eqidd
` |-  ( ( X e. Word B /\ C e. B ) -> ( # ` X ) = ( # ` X ) )`
44 ccats1val2
` |-  ( ( X e. Word B /\ C e. B /\ ( # ` X ) = ( # ` X ) ) -> ( ( X ++ <" C "> ) ` ( # ` X ) ) = C )`
45 44 fveq1d
` |-  ( ( X e. Word B /\ C e. B /\ ( # ` X ) = ( # ` X ) ) -> ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( C ` n ) )`
46 43 45 mpd3an3
` |-  ( ( X e. Word B /\ C e. B ) -> ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( C ` n ) )`
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( C ` n ) )`
48 ccats1val2
` |-  ( ( Y e. Word P /\ R e. P /\ ( # ` X ) = ( # ` Y ) ) -> ( ( Y ++ <" R "> ) ` ( # ` X ) ) = R )`
49 48 fveq1d
` |-  ( ( Y e. Word P /\ R e. P /\ ( # ` X ) = ( # ` Y ) ) -> ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) = ( R ` n ) )`
50 49 3expa
` |-  ( ( ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) = ( R ` n ) )`
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) = ( R ` n ) )`
52 47 51 eqeq12d
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) <-> ( C ` n ) = ( R ` n ) ) )`
53 52 ralbidv
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( A. n e. I ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) <-> A. n e. I ( C ` n ) = ( R ` n ) ) )`
54 42 53 anbi12d
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) /\ A. n e. I ( ( ( X ++ <" C "> ) ` ( # ` X ) ) ` n ) = ( ( ( Y ++ <" R "> ) ` ( # ` X ) ) ` n ) ) <-> ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) /\ A. n e. I ( C ` n ) = ( R ` n ) ) ) )`
55 16 26 54 3bitrd
` |-  ( ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) -> ( A. i e. ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) /\ A. n e. I ( C ` n ) = ( R ` n ) ) ) )`
` |-  ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R 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 ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) <-> ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) /\ A. n e. I ( C ` n ) = ( R ` n ) ) ) )`
57 pm3.35
` |-  ( ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` 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 ) ) ) -> A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) )`
58 fveq2
` |-  ( n = j -> ( ( S gsum X ) ` n ) = ( ( S gsum X ) ` j ) )`
59 fveq2
` |-  ( n = j -> ( ( Z gsum Y ) ` n ) = ( ( Z gsum Y ) ` j ) )`
60 58 59 eqeq12d
` |-  ( n = j -> ( ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) <-> ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) )`
61 60 cbvralvw
` |-  ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) <-> A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) )`
62 simp-4l
` |-  ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) -> N e. Fin )`
63 simp-4r
` |-  ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) -> M e. Fin )`
64 simpr
` |-  ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) -> n e. I )`
65 62 63 64 3jca
` |-  ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) -> ( N e. Fin /\ M e. Fin /\ n e. I ) )`
` |-  ( ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) /\ ( C ` n ) = ( R ` n ) ) -> ( N e. Fin /\ M e. Fin /\ n e. I ) )`
67 simp-4r
` |-  ( ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) /\ ( C ` n ) = ( R ` n ) ) -> ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) )`
68 simplr
` |-  ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) -> A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) )`
69 68 anim1i
` |-  ( ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) /\ ( C ` n ) = ( R ` n ) ) -> ( A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) /\ ( C ` n ) = ( R ` n ) ) )`
70 1 2 3 4 5 gsmsymgreqlem1
` |-  ( ( ( N e. Fin /\ M e. Fin /\ n e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( ( A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) /\ ( C ` n ) = ( R ` n ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) )`
71 70 imp
` |-  ( ( ( ( N e. Fin /\ M e. Fin /\ n e. I ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ ( A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) /\ ( C ` n ) = ( R ` n ) ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) )`
72 66 67 69 71 syl21anc
` |-  ( ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) /\ ( C ` n ) = ( R ` n ) ) -> ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) )`
73 72 ex
` |-  ( ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) /\ n e. I ) -> ( ( C ` n ) = ( R ` n ) -> ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) )`
74 73 ralimdva
` |-  ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) /\ A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) ) -> ( A. n e. I ( C ` n ) = ( R ` n ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) )`
75 74 expcom
` |-  ( A. j e. I ( ( S gsum X ) ` j ) = ( ( Z gsum Y ) ` j ) -> ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( A. n e. I ( C ` n ) = ( R ` n ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`
76 61 75 sylbi
` |-  ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) -> ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> ( A. n e. I ( C ` n ) = ( R ` n ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`
77 76 com23
` |-  ( A. n e. I ( ( S gsum X ) ` n ) = ( ( Z gsum Y ) ` n ) -> ( A. n e. I ( C ` n ) = ( R ` n ) -> ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`
78 57 77 syl
` |-  ( ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` 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 ) ) ) -> ( A. n e. I ( C ` n ) = ( R ` n ) -> ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`
79 78 impancom
` |-  ( ( A. i e. ( 0 ..^ ( # ` X ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) /\ A. n e. I ( C ` n ) = ( R ` 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 ) ) -> ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R e. P ) /\ ( # ` X ) = ( # ` Y ) ) ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`
80 79 com13
` |-  ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R 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 ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) /\ A. n e. I ( C ` n ) = ( R ` n ) ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`
81 80 imp
` |-  ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R 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 ) ) A. n e. I ( ( X ` i ) ` n ) = ( ( Y ` i ) ` n ) /\ A. n e. I ( C ` n ) = ( R ` n ) ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) )`
82 56 81 sylbid
` |-  ( ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R 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 ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) )`
83 82 ex
` |-  ( ( ( N e. Fin /\ M e. Fin ) /\ ( ( X e. Word B /\ C e. B ) /\ ( Y e. Word P /\ R 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 ++ <" C "> ) ) ) A. n e. I ( ( ( X ++ <" C "> ) ` i ) ` n ) = ( ( ( Y ++ <" R "> ) ` i ) ` n ) -> A. n e. I ( ( S gsum ( X ++ <" C "> ) ) ` n ) = ( ( Z gsum ( Y ++ <" R "> ) ) ` n ) ) ) )`