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

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 sselid 
 |-  ( ( ( 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 56 grpmndd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> H e. Mnd )
58 wrdco 
 |-  ( ( ( x prefix n ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( x prefix n ) ) e. Word B )
59 50 52 58 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( x prefix n ) ) e. Word B )
60 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 )
61 42 52 60 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 )
62 eqid 
 |-  ( +g ` H ) = ( +g ` H )
63 1 62 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 ) >. "> ) ) ) )
64 57 59 61 63 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 ) >. "> ) ) ) )
65 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 ) >. ) "> )
66 df-ov 
 |-  ( a T b ) = ( T ` <. a , b >. )
67 66 a1i 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( a T b ) = ( T ` <. a , b >. ) )
68 66 fveq2i 
 |-  ( N ` ( a T b ) ) = ( N ` ( T ` <. a , b >. ) )
69 df-ov 
 |-  ( a ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) b ) = ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. )
70 eqid 
 |-  ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
71 70 efgmval 
 |-  ( ( a e. I /\ b e. 2o ) -> ( a ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) b ) = <. a , ( 1o \ b ) >. )
72 69 71 eqtr3id 
 |-  ( ( a e. I /\ b e. 2o ) -> ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) = <. a , ( 1o \ b ) >. )
73 72 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 ) >. )
74 73 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 ) >. ) )
75 1 2 3 4 5 6 70 frgpuptinv 
 |-  ( ( ph /\ <. a , b >. e. ( I X. 2o ) ) -> ( T ` ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) ) = ( N ` ( T ` <. a , b >. ) ) )
76 36 75 sylan2 
 |-  ( ( ph /\ ( a e. I /\ b e. 2o ) ) -> ( T ` ( ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. ) ` <. a , b >. ) ) = ( N ` ( T ` <. a , b >. ) ) )
77 76 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 >. ) ) )
78 74 77 eqtr3d 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T ` <. a , ( 1o \ b ) >. ) = ( N ` ( T ` <. a , b >. ) ) )
79 68 78 eqtr4id 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( N ` ( a T b ) ) = ( T ` <. a , ( 1o \ b ) >. ) )
80 67 79 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 ) >. ) "> )
81 65 80 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 ) ) "> )
82 81 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 ) ) "> ) )
83 simprr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> b e. 2o )
84 52 38 83 fovcdmd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( a T b ) e. B )
85 1 2 grpinvcl 
 |-  ( ( H e. Grp /\ ( a T b ) e. B ) -> ( N ` ( a T b ) ) e. B )
86 56 84 85 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( N ` ( a T b ) ) e. B )
87 1 62 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 ) ) ) )
88 57 84 86 87 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 ) ) ) )
89 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
90 1 62 89 2 grprinv 
 |-  ( ( H e. Grp /\ ( a T b ) e. B ) -> ( ( a T b ) ( +g ` H ) ( N ` ( a T b ) ) ) = ( 0g ` H ) )
91 56 84 90 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 ) )
92 82 88 91 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 ) )
93 92 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 ) ) )
94 1 gsumwcl 
 |-  ( ( H e. Mnd /\ ( T o. ( x prefix n ) ) e. Word B ) -> ( H gsum ( T o. ( x prefix n ) ) ) e. B )
95 57 59 94 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( H gsum ( T o. ( x prefix n ) ) ) e. B )
96 1 62 89 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 ) ) ) )
97 56 95 96 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 ) ) ) )
98 93 97 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 ) ) ) )
99 55 64 98 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 ) >. "> ) ) ) )
100 99 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 ) >. ) ) ) ) )
101 swrdcl 
 |-  ( x e. Word ( I X. 2o ) -> ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) )
102 35 101 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) )
103 wrdco 
 |-  ( ( ( x substr <. n , ( # ` x ) >. ) e. Word ( I X. 2o ) /\ T : ( I X. 2o ) --> B ) -> ( T o. ( x substr <. n , ( # ` x ) >. ) ) e. Word B )
104 102 52 103 syl2anc 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( T o. ( x substr <. n , ( # ` x ) >. ) ) e. Word B )
105 1 62 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 ) >. ) ) ) ) )
106 57 59 104 105 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 ) >. ) ) ) ) )
107 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 ) )
108 50 42 107 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 ) )
109 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 )
110 108 52 109 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 )
111 1 62 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 ) >. ) ) ) ) )
112 57 110 104 111 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 ) >. ) ) ) ) )
113 100 106 112 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 ) >. ) ) ) ) )
114 simplrr 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> n e. ( 0 ... ( # ` x ) ) )
115 lencl 
 |-  ( x e. Word ( I X. 2o ) -> ( # ` x ) e. NN0 )
116 35 115 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( # ` x ) e. NN0 )
117 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
118 116 117 eleqtrdi 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( # ` x ) e. ( ZZ>= ` 0 ) )
119 eluzfz2 
 |-  ( ( # ` x ) e. ( ZZ>= ` 0 ) -> ( # ` x ) e. ( 0 ... ( # ` x ) ) )
120 118 119 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( # ` x ) e. ( 0 ... ( # ` x ) ) )
121 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 ) ) )
122 35 114 120 121 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 ) ) )
123 pfxid 
 |-  ( x e. Word ( I X. 2o ) -> ( x prefix ( # ` x ) ) = x )
124 35 123 syl 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( x prefix ( # ` x ) ) = x )
125 122 124 eqtrd 
 |-  ( ( ( ph /\ ( x e. W /\ n e. ( 0 ... ( # ` x ) ) ) ) /\ ( a e. I /\ b e. 2o ) ) -> ( ( x prefix n ) ++ ( x substr <. n , ( # ` x ) >. ) ) = x )
126 125 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 ) )
127 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 ) >. ) ) ) )
128 50 102 52 127 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 ) >. ) ) ) )
129 126 128 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 ) >. ) ) ) )
130 129 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 ) >. ) ) ) ) )
131 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 ) >. ) ) )
132 32 114 114 42 131 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 ) >. ) ) )
133 132 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 ) >. ) ) ) )
134 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 ) >. ) ) ) )
135 108 102 52 134 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 ) >. ) ) ) )
136 133 135 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 ) >. ) ) ) )
137 136 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 ) >. ) ) ) ) )
138 113 130 137 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 ) >. "> >. ) ) ) )
139 vex 
 |-  x e. _V
140 ovex 
 |-  ( x splice <. n , n , <" <. a , b >. <. a , ( 1o \ b ) >. "> >. ) e. _V
141 eleq1 
 |-  ( u = x -> ( u e. W <-> x e. W ) )
142 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 ) )
143 141 142 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 ) ) )
144 25 143 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 ) ) )
145 coeq2 
 |-  ( u = x -> ( T o. u ) = ( T o. x ) )
146 145 oveq2d 
 |-  ( u = x -> ( H gsum ( T o. u ) ) = ( H gsum ( T o. x ) ) )
147 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 ) >. "> >. ) ) )
148 147 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 ) >. "> >. ) ) ) )
149 146 148 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 ) >. "> >. ) ) ) ) )
150 144 149 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 ) >. "> >. ) ) ) ) ) )
151 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 ) ) ) }
152 139 140 150 151 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 ) >. "> >. ) ) ) ) )
153 32 48 138 152 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 ) >. "> >. ) )
154 153 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 ) >. "> >. ) )
155 154 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 ) >. "> >. ) )
156 7 fvexi 
 |-  W e. _V
157 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 ) )
158 31 156 157 mpisyl 
 |-  ( ph -> { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } e. _V )
159 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 ) )
160 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 ) >. "> >. ) ) )
161 160 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 ) >. "> >. ) ) )
162 161 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 ) >. "> >. ) ) )
163 159 162 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 ) >. "> >. ) ) ) )
164 163 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 ) >. "> >. ) ) ) )
165 158 164 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 ) >. "> >. ) ) ) )
166 31 155 165 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 ) >. "> >. ) ) } )
167 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 ) ) ) } )
168 166 167 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 ) ) ) } )
169 9 168 eqsstrid 
 |-  ( ph -> .~ C_ { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } )
170 169 ssbrd 
 |-  ( ph -> ( A .~ C -> A { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } C ) )
171 170 imp 
 |-  ( ( ph /\ A .~ C ) -> A { <. u , v >. | ( { u , v } C_ W /\ ( H gsum ( T o. u ) ) = ( H gsum ( T o. v ) ) ) } C )
172 7 8 efger 
 |-  .~ Er W
173 errel 
 |-  ( .~ Er W -> Rel .~ )
174 172 173 mp1i 
 |-  ( ph -> Rel .~ )
175 brrelex12 
 |-  ( ( Rel .~ /\ A .~ C ) -> ( A e. _V /\ C e. _V ) )
176 174 175 sylan 
 |-  ( ( ph /\ A .~ C ) -> ( A e. _V /\ C e. _V ) )
177 preq12 
 |-  ( ( u = A /\ v = C ) -> { u , v } = { A , C } )
178 177 sseq1d 
 |-  ( ( u = A /\ v = C ) -> ( { u , v } C_ W <-> { A , C } C_ W ) )
179 coeq2 
 |-  ( u = A -> ( T o. u ) = ( T o. A ) )
180 179 oveq2d 
 |-  ( u = A -> ( H gsum ( T o. u ) ) = ( H gsum ( T o. A ) ) )
181 coeq2 
 |-  ( v = C -> ( T o. v ) = ( T o. C ) )
182 181 oveq2d 
 |-  ( v = C -> ( H gsum ( T o. v ) ) = ( H gsum ( T o. C ) ) )
183 180 182 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 ) ) ) )
184 178 183 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 ) ) ) ) )
185 184 151 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 ) ) ) ) )
186 176 185 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 ) ) ) ) )
187 171 186 mpbid 
 |-  ( ( ph /\ A .~ C ) -> ( { A , C } C_ W /\ ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) ) )
188 187 simprd 
 |-  ( ( ph /\ A .~ C ) -> ( H gsum ( T o. A ) ) = ( H gsum ( T o. C ) ) )