This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) } ) )
14 13 adantr 
 |-  ( ( X e. Word B /\ C e. B ) -> ( 0 ..^ ( # ` ( X ++ <" C "> ) ) ) = ( ( 0 ..^ ( # ` X ) ) u. { ( # ` X ) } ) )
15 14 3ad2ant1 
 |-  ( ( ( 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 ) ) )
17 8 adantr 
 |-  ( ( X e. Word B /\ C e. B ) -> ( # ` X ) e. NN0 )
18 17 3ad2ant1 
 |-  ( ( ( 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 ) ) ) )
35 34 3ad2ant3 
 |-  ( ( ( 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 ) )
47 46 3ad2ant1 
 |-  ( ( ( 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 ) )
51 50 3adant1 
 |-  ( ( ( 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 ) ) ) )
56 55 ad2antlr 
 |-  ( ( ( ( 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 ) )
66 65 adantr 
 |-  ( ( ( ( ( ( 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 ) ) ) )