Metamath Proof Explorer

Theorem frgpuplem

Description: Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses frgpup.b 
|- B = ( Base ` H )
frgpup.n 
|- N = ( invg ` H )
frgpup.t 
|- T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
frgpup.h 
|- ( ph -> H e. Grp )
frgpup.i 
|- ( ph -> I e. V )
frgpup.a 
|- ( ph -> F : I --> B )
frgpup.w 
|- W = ( _I ` Word ( I X. 2o ) )
frgpup.r 
|- .~ = ( ~FG ` I )
Assertion frgpuplem 
|- ( ( ph /\ A .~ C ) -> ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) )

Proof

Step Hyp Ref Expression
1 frgpup.b 
 |-  B = ( Base ` H )
2 frgpup.n 
 |-  N = ( invg ` H )
3 frgpup.t 
 |-  T = ( y e. I , z e. 2o |-> if ( z = (/) , ( F ` y ) , ( N ` ( F ` y ) ) ) )
4 frgpup.h 
 |-  ( ph -> H e. Grp )
5 frgpup.i 
 |-  ( ph -> I e. V )
6 frgpup.a 
 |-  ( ph -> F : I --> B )
7 frgpup.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
8 frgpup.r 
 |-  .~ = ( ~FG ` I )
9 7 8 efgval 
 |-  .~ = |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) }
10 coeq2 
 |-  ( u = v -> ( T o. u ) = ( T o. v ) )
11 10 oveq2d 
 |-  ( u = v -> ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) )
12 eqid 
 |-  { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } = { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) }
13 11 12 eqer 
 |-  { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } Er _V
14 13 a1i 
 |-  ( ph -> { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } Er _V )
15 ssv 
 |-  W C_ _V
16 15 a1i 
 |-  ( ph -> W C_ _V )
17 14 16 erinxp 
 |-  ( ph -> ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) ) Er W )
18 df-xp 
 |-  ( W X. W ) = { <. u , v >. | ( u e. W /\ v e. W ) }
19 18 ineq1i 
 |-  ( ( W X. W ) i^i { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } ) = ( { <. u , v >. | ( u e. W /\ v e. W ) } i^i { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } )
20 incom 
 |-  ( ( W X. W ) i^i { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } ) = ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) )
21 inopab 
 |-  ( { <. u , v >. | ( u e. W /\ v e. W ) } i^i { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } ) = { <. u , v >. | ( ( u e. W /\ v e. W ) /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) }
22 19 20 21 3eqtr3i 
 |-  ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) ) = { <. u , v >. | ( ( u e. W /\ v e. W ) /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) }
23 vex 
 |-  u e. _V
24 vex 
 |-  v e. _V
25 23 24 prss 
 |-  ( ( u e. W /\ v e. W ) <-> { u , v } C_ W )
26 25 anbi1i 
 |-  ( ( ( u e. W /\ v e. W ) /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) <-> ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) )
27 26 opabbii 
 |-  { <. u , v >. | ( ( u e. W /\ v e. W ) /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) }
28 22 27 eqtri 
 |-  ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) ) = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) }
29 ereq1 
 |-  ( ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) ) = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } -> ( ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) ) Er W <-> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W ) )
30 28 29 ax-mp 
 |-  ( ( { <. u , v >. | ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) } i^i ( W X. W ) ) Er W <-> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W )
31 17 30 sylib 
 |-  ( ph -> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W )
32 simplrl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> x e. W )
33 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
34 7 33 eqsstri 
 |-  W C_ Word ( I X. 2o )
35 34 32 sseldi 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> x e. Word ( I X. 2o ) )
36 opelxpi 
 |-  ( ( a e. I /\ b e. 2o ) -> <. a , b >. e. ( I X. 2o ) )
37 36 adantl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> <. a , b >. e. ( I X. 2o ) )
38 simprl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> a e. I )
39 2oconcl 
 |-  ( b e. 2o -> ( 1o \ b ) e. 2o )
40 39 ad2antll 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( 1o \ b ) e. 2o )
41 38 40 opelxpd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> <. a , ( 1o \ b ) >. e. ( I X. 2o ) )
42 37 41 s2cld 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> <" <. a , b >. <. a , ( 1o \ b ) >. "> e. Word ( I X. 2o ) )
43 splcl 
 |-  ( ( x e. Word ( I X. 2o ) /\ <" <. a , b >. <. a , ( 1o \ b ) >. "> e. Word ( I X. 2o ) ) -> ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. Word ( I X. 2o ) )
44 35 42 43 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. Word ( I X. 2o ) )
45 7 efgrcl 
 |-  ( x e. W -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
46 32 45 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( I e. _V /\ W = Word ( I X. 2o ) ) )
47 46 simprd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> W = Word ( I X. 2o ) )
48 44 47 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. W )
49 pfxcl 
 |-  ( x e. Word ( I X. 2o ) -> ( x prefix n ) e. Word ( I X. 2o ) )
50 35 49 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x prefix n ) e. Word ( I X. 2o ) )
51 1 2 3 4 5 6 frgpuptf 
 |-  ( ph -> T : ( I X. 2o ) --> B )
52 51 ad2antrr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> T : ( I X. 2o ) --> B )
53 ccatco 
 |-  ( ( ( x prefix n ) e. Word ( I X. 2o ) /\ <" <. a , b >. <. a , ( 1o \ b ) >. "> e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) = ( ( T o. ( x prefix n ) ) ++ ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) )
54 50 42 52 53 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) = ( ( T o. ( x prefix n ) ) ++ ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) )
55 54 oveq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) = ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) )
56 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> H e. Grp )
57 grpmnd 
 |-  ( H e. Grp -> H e. Mnd )
58 56 57 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> H e. Mnd )
59 wrdco 
 |-  ( ( ( x prefix n ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( x prefix n ) ) e. Word B )
60 50 52 59 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( x prefix n ) ) e. Word B )
61 wrdco 
 |-  ( ( <" <. a , b >. <. a , ( 1o \ b ) >. "> e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word B )
62 42 52 61 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word B )
63 eqid 
 |-  ( +g ` H ) = ( +g ` H )
64 1 63 gsumccat 
 |-  ( ( H e. Mnd /\ ( T o. ( x prefix n ) ) e. Word B /\ ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word B ) -> ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) = ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) )
65 58 60 62 64 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) = ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) )
66 52 37 41 s2co 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) = <" ( T ` <. a , b >. ) ( T ` <. a , ( 1o \ b ) >. ) "> )
67 df-ov 
 |-  ( a T b ) = ( T ` <. a , b >. )
68 67 a1i 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( a T b ) = ( T ` <. a , b >. ) )
69 67 fveq2i 
 |-  ( N ` ( a T b ) ) = ( N ` ( T ` <. a , b >. ) )
70 df-ov 
 |-  ( a ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) b ) = ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. )
71 eqid 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
72 71 efgmval 
 |-  ( ( a e. I /\ b e. 2o ) -> ( a ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) b ) = <. a , ( 1o \ b ) >. )
73 70 72 eqtr3id 
 |-  ( ( a e. I /\ b e. 2o ) -> ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) = <. a , ( 1o \ b ) >. )
74 73 adantl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) = <. a , ( 1o \ b ) >. )
75 74 fveq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) ) = ( T ` <. a , ( 1o \ b ) >. ) )
76 1 2 3 4 5 6 71 frgpuptinv 
 |-  ( ( ph /\ <. a , b >. e. ( I X. 2o ) ) -> ( T ` ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) ) = ( N ` ( T ` <. a , b >. ) ) )
77 36 76 sylan2 
 |-  ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) ) = ( N ` ( T ` <. a , b >. ) ) )
78 77 adantlr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) ) = ( N ` ( T ` <. a , b >. ) ) )
79 75 78 eqtr3d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T ` <. a , ( 1o \ b ) >. ) = ( N ` ( T ` <. a , b >. ) ) )
80 69 79 eqtr4id 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( N ` ( a T b ) ) = ( T ` <. a , ( 1o \ b ) >. ) )
81 68 80 s2eqd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> <" ( a T b ) ( N ` ( a T b ) ) "> = <" ( T ` <. a , b >. ) ( T ` <. a , ( 1o \ b ) >. ) "> )
82 66 81 eqtr4d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) = <" ( a T b ) ( N ` ( a T b ) ) "> )
83 82 oveq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) = ( H gsum <" ( a T b ) ( N ` ( a T b ) ) "> ) )
84 simprr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> b e. 2o )
85 52 38 84 fovrnd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( a T b ) e. B )
86 1 2 grpinvcl 
 |-  ( ( H e. Grp /\ ( a T b ) e. B ) -> ( N ` ( a T b ) ) e. B )
87 56 85 86 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( N ` ( a T b ) ) e. B )
88 1 63 gsumws2 
 |-  ( ( H e. Mnd /\ ( a T b ) e. B /\ ( N ` ( a T b ) ) e. B ) -> ( H gsum <" ( a T b ) ( N ` ( a T b ) ) "> ) = ( ( a T b ) ( +g ` H ) ( N ` ( a T b ) ) ) )
89 58 85 87 88 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum <" ( a T b ) ( N ` ( a T b ) ) "> ) = ( ( a T b ) ( +g ` H ) ( N ` ( a T b ) ) ) )
90 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
91 1 63 90 2 grprinv 
 |-  ( ( H e. Grp /\ ( a T b ) e. B ) -> ( ( a T b ) ( +g ` H ) ( N ` ( a T b ) ) ) = ( 0g ` H ) )
92 56 85 91 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( a T b ) ( +g ` H ) ( N ` ( a T b ) ) ) = ( 0g ` H ) )
93 83 89 92 3eqtrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) = ( 0g ` H ) )
94 93 oveq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) = ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( 0g ` H ) ) )
95 1 gsumwcl 
 |-  ( ( H e. Mnd /\ ( T o. ( x prefix n ) ) e. Word B ) -> ( H gsum ( T o. ( x prefix n ) ) ) e. B )
96 58 60 95 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. ( x prefix n ) ) ) e. B )
97 1 63 90 grprid 
 |-  ( ( H e. Grp /\ ( H gsum ( T o. ( x prefix n ) ) ) e. B ) -> ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( 0g ` H ) ) = ( H gsum ( T o. ( x prefix n ) ) ) )
98 56 96 97 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( 0g ` H ) ) = ( H gsum ( T o. ( x prefix n ) ) ) )
99 94 98 eqtrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) = ( H gsum ( T o. ( x prefix n ) ) ) )
100 55 65 99 3eqtrrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. ( x prefix n ) ) ) = ( H gsum ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) )
101 100 oveq1d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) = ( ( H gsum ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) ( +g ` H ) ( H gsum ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
102 swrdcl 
 |-  ( x e. Word ( I X. 2o ) -> ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) )
103 35 102 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) )
104 wrdco 
 |-  ( ( ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( x substr <. n , ( # ` x ) >. ) ) e. Word B )
105 103 52 104 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( x substr <. n , ( # ` x ) >. ) ) e. Word B )
106 1 63 gsumccat 
 |-  ( ( H e. Mnd /\ ( T o. ( x prefix n ) ) e. Word B /\ ( T o. ( x substr <. n , ( # ` x ) >. ) ) e. Word B ) -> ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) = ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
107 58 60 105 106 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) = ( ( H gsum ( T o. ( x prefix n ) ) ) ( +g ` H ) ( H gsum ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
108 ccatcl 
 |-  ( ( ( x prefix n ) e. Word ( I X. 2o ) /\ <" <. a , b >. <. a , ( 1o \ b ) >. "> e. Word ( I X. 2o ) ) -> ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word ( I X. 2o ) )
109 50 42 108 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word ( I X. 2o ) )
110 wrdco 
 |-  ( ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) e. Word B )
111 109 52 110 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) e. Word B )
112 1 63 gsumccat 
 |-  ( ( H e. Mnd /\ ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) e. Word B /\ ( T o. ( x substr <. n , ( # ` x ) >. ) ) e. Word B ) -> ( H gsum ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) = ( ( H gsum ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) ( +g ` H ) ( H gsum ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
113 58 111 105 112 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) = ( ( H gsum ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ) ( +g ` H ) ( H gsum ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
114 101 107 113 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) = ( H gsum ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
115 simplrr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> n e. ( 0 ... ( # ` x ) ) )
116 lencl 
 |-  ( x e. Word ( I X. 2o ) -> ( # ` x ) e. NN0 )
117 35 116 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( # ` x ) e. NN0 )
118 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
119 117 118 eleqtrdi 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( # ` x ) e. ( ZZ>= ` 0 ) )
120 eluzfz2 
 |-  ( ( # ` x ) e. ( ZZ>= ` 0 ) -> ( # ` x ) e. ( 0 ... ( # ` x ) ) )
121 119 120 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( # ` x ) e. ( 0 ... ( # ` x ) ) )
122 ccatpfx 
 |-  ( ( x e. Word ( I X. 2o ) /\ n e. ( 0 ... ( # ` x ) ) /\ ( # ` x ) e. ( 0 ... ( # ` x ) ) ) -> ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) = ( x prefix ( # ` x ) ) )
123 35 115 121 122 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) = ( x prefix ( # ` x ) ) )
124 pfxid 
 |-  ( x e. Word ( I X. 2o ) -> ( x prefix ( # ` x ) ) = x )
125 35 124 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x prefix ( # ` x ) ) = x )
126 123 125 eqtrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) = x )
127 126 coeq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) ) = ( T o. x ) )
128 ccatco 
 |-  ( ( ( x prefix n ) e. Word ( I X. 2o ) /\ ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) ) = ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) )
129 50 103 52 128 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) ) = ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) )
130 127 129 eqtr3d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. x ) = ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) )
131 130 oveq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. x ) ) = ( H gsum ( ( T o. ( x prefix n ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
132 splval 
 |-  ( ( x e. W /\ ( n e. ( 0 ... ( # ` x ) ) /\ n e. ( 0 ... ( # ` x ) ) /\ <" <. a , b >. <. a , ( 1o \ b ) >. "> e. Word ( I X. 2o ) ) ) -> ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) = ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ++ ( x substr <. n , ( # ` x ) >. ) ) )
133 32 115 115 42 132 syl13anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) = ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ++ ( x substr <. n , ( # ` x ) >. ) ) )
134 133 coeq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) = ( T o. ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ++ ( x substr <. n , ( # ` x ) >. ) ) ) )
135 ccatco 
 |-  ( ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) e. Word ( I X. 2o ) /\ ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ++ ( x substr <. n , ( # ` x ) >. ) ) ) = ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) )
136 109 103 52 135 syl3anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ++ ( x substr <. n , ( # ` x ) >. ) ) ) = ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) )
137 134 136 eqtrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) = ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) )
138 137 oveq2d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) = ( H gsum ( ( T o. ( ( x prefix n ) ++ <" <. a , b >. <. a , ( 1o \ b ) >. "> ) ) ++ ( T o. ( x substr <. n , ( # ` x ) >. ) ) ) ) )
139 114 131 138 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. x ) ) = ( H gsum ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) )
140 vex 
 |-  x e. _V
141 ovex 
 |-  ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. _V
142 eleq1 
 |-  ( u = x -> ( u e. W <-> x e. W ) )
143 eleq1 
 |-  ( v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> ( v e. W <-> ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. W ) )
144 142 143 bi2anan9 
 |-  ( ( u = x /\ v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> ( ( u e. W /\ v e. W ) <-> ( x e. W /\ ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. W ) ) )
145 25 144 bitr3id 
 |-  ( ( u = x /\ v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> ( { u , v } C_ W <-> ( x e. W /\ ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. W ) ) )
146 coeq2 
 |-  ( u = x -> ( T o. u ) = ( T o. x ) )
147 146 oveq2d 
 |-  ( u = x -> ( H gsum ( T o. u ) ) = ( H gsum ( T o. x ) ) )
148 coeq2 
 |-  ( v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> ( T o. v ) = ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
149 148 oveq2d 
 |-  ( v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) -> ( H gsum ( T o. v ) ) = ( H gsum ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) )
150 147 149 eqeqan12d 
 |-  ( ( u = x /\ v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> ( ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) <-> ( H gsum ( T o. x ) ) = ( H gsum ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) ) )
151 145 150 anbi12d 
 |-  ( ( u = x /\ v = ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) -> ( ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) <-> ( ( x e. W /\ ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. W ) /\ ( H gsum ( T o. x ) ) = ( H gsum ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) ) ) )
152 eqid 
 |-  { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) }
153 140 141 151 152 braba 
 |-  ( x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> ( ( x e. W /\ ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. W ) /\ ( H gsum ( T o. x ) ) = ( H gsum ( T o. ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) ) )
154 32 48 139 153 syl21anbrc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
155 154 ralrimivva 
 |-  ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) -> A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
156 155 ralrimivva 
 |-  ( ph -> A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) )
157 7 fvexi 
 |-  W e. _V
158 erex 
 |-  ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W -> ( W e. _V -> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. _V ) )
159 31 157 158 mpisyl 
 |-  ( ph -> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. _V )
160 ereq1 
 |-  ( r = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } -> ( r Er W <-> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W ) )
161 breq 
 |-  ( r = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } -> ( x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
162 161 2ralbidv 
 |-  ( r = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } -> ( A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
163 162 2ralbidv 
 |-  ( r = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } -> ( A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) <-> A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) )
164 160 163 anbi12d 
 |-  ( r = { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } -> ( ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) <-> ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) )
165 164 elabg 
 |-  ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. _V -> ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } <-> ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) )
166 159 165 syl 
 |-  ( ph -> ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } <-> ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) ) )
167 31 156 166 mpbir2and 
 |-  ( ph -> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } )
168 intss1 
 |-  ( { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } C_ { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } )
169 167 168 syl 
 |-  ( ph -> |^| { r | ( r Er W /\ A. x e. W A. n e. ( 0 ... ( # ` x ) ) A. a e. I A. b e. 2o x r ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) ) } C_ { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } )
170 9 169 eqsstrid 
 |-  ( ph -> .~ C_ { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } )
171 170 ssbrd 
 |-  ( ph -> ( A .~ C -> A { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } C ) )
172 171 imp 
 |-  ( ( ph /\ A .~ C ) -> A { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } C )
173 7 8 efger 
 |-  .~ Er W
174 errel 
 |-  ( .~ Er W -> Rel .~ )
175 173 174 mp1i 
 |-  ( ph -> Rel .~ )
176 brrelex12 
 |-  ( ( Rel .~ /\ A .~ C ) -> ( A e. _V /\ C e. _V ) )
177 175 176 sylan 
 |-  ( ( ph /\ A .~ C ) -> ( A e. _V /\ C e. _V ) )
178 preq12 
 |-  ( ( u = A /\ v = C ) -> { u , v } = { A , C } )
179 178 sseq1d 
 |-  ( ( u = A /\ v = C ) -> ( { u , v } C_ W <-> { A , C } C_ W ) )
180 coeq2 
 |-  ( u = A -> ( T o. u ) = ( T o. A ) )
181 180 oveq2d 
 |-  ( u = A -> ( H gsum ( T o. u ) ) = ( H gsum ( T o. A ) ) )
182 coeq2 
 |-  ( v = C -> ( T o. v ) = ( T o. C ) )
183 182 oveq2d 
 |-  ( v = C -> ( H gsum ( T o. v ) ) = ( H gsum ( T o. C ) ) )
184 181 183 eqeqan12d 
 |-  ( ( u = A /\ v = C ) -> ( ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) <-> ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) ) )
185 179 184 anbi12d 
 |-  ( ( u = A /\ v = C ) -> ( ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) <-> ( { A , C } C_ W /\ ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) ) ) )
186 185 152 brabga 
 |-  ( ( A e. _V /\ C e. _V ) -> ( A { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } C <-> ( { A , C } C_ W /\ ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) ) ) )
187 177 186 syl 
 |-  ( ( ph /\ A .~ C ) -> ( A { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } C <-> ( { A , C } C_ W /\ ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) ) ) )
188 172 187 mpbid 
 |-  ( ( ph /\ A .~ C ) -> ( { A , C } C_ W /\ ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) ) )
189 188 simprd 
 |-  ( ( ph /\ A .~ C ) -> ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) )