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
|
fovrnd |
|- ( ( ( 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 ) ) ) |