Metamath Proof Explorer

Theorem gsumvalx

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses gsumval.b 
|- B = ( Base ` G )
gsumval.z 
|- .0. = ( 0g ` G )
gsumval.p 
|- .+ = ( +g ` G )
gsumval.o 
|- O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }
gsumval.w 
|- ( ph -> W = ( `' F " ( _V \ O ) ) )
gsumval.g 
|- ( ph -> G e. V )
gsumvalx.f 
|- ( ph -> F e. X )
gsumvalx.a 
|- ( ph -> dom F = A )
Assertion gsumvalx 
|- ( ph -> ( G gsum F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumval.b 
 |-  B = ( Base ` G )
2 gsumval.z 
 |-  .0. = ( 0g ` G )
3 gsumval.p 
 |-  .+ = ( +g ` G )
4 gsumval.o 
 |-  O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }
5 gsumval.w 
 |-  ( ph -> W = ( `' F " ( _V \ O ) ) )
6 gsumval.g 
 |-  ( ph -> G e. V )
7 gsumvalx.f 
 |-  ( ph -> F e. X )
8 gsumvalx.a 
 |-  ( ph -> dom F = A )
9 df-gsum 
 |-  gsum = ( w e. _V , g e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) )
10 9 a1i 
 |-  ( ph -> gsum = ( w e. _V , g e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) ) )
11 simprl 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> w = G )
12 11 fveq2d 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( Base ` w ) = ( Base ` G ) )
13 12 1 eqtr4di 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( Base ` w ) = B )
14 11 fveq2d 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( +g ` w ) = ( +g ` G ) )
15 14 3 eqtr4di 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( +g ` w ) = .+ )
16 15 oveqd 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( x ( +g ` w ) y ) = ( x .+ y ) )
17 16 eqeq1d 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( x ( +g ` w ) y ) = y <-> ( x .+ y ) = y ) )
18 15 oveqd 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( y ( +g ` w ) x ) = ( y .+ x ) )
19 18 eqeq1d 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( y ( +g ` w ) x ) = y <-> ( y .+ x ) = y ) )
20 17 19 anbi12d 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) <-> ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
21 13 20 raleqbidv 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> ( A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
22 13 21 rabeqbidv 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } )
23 oveq2 
 |-  ( t = y -> ( s .+ t ) = ( s .+ y ) )
24 id 
 |-  ( t = y -> t = y )
25 23 24 eqeq12d 
 |-  ( t = y -> ( ( s .+ t ) = t <-> ( s .+ y ) = y ) )
26 oveq1 
 |-  ( t = y -> ( t .+ s ) = ( y .+ s ) )
27 26 24 eqeq12d 
 |-  ( t = y -> ( ( t .+ s ) = t <-> ( y .+ s ) = y ) )
28 25 27 anbi12d 
 |-  ( t = y -> ( ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> ( ( s .+ y ) = y /\ ( y .+ s ) = y ) ) )
29 28 cbvralvw 
 |-  ( A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> A. y e. B ( ( s .+ y ) = y /\ ( y .+ s ) = y ) )
30 oveq1 
 |-  ( s = x -> ( s .+ y ) = ( x .+ y ) )
31 30 eqeq1d 
 |-  ( s = x -> ( ( s .+ y ) = y <-> ( x .+ y ) = y ) )
32 31 ovanraleqv 
 |-  ( s = x -> ( A. y e. B ( ( s .+ y ) = y /\ ( y .+ s ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
33 29 32 syl5bb 
 |-  ( s = x -> ( A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
34 33 cbvrabv 
 |-  { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) } = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
35 4 34 eqtri 
 |-  O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
36 22 35 eqtr4di 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } = O )
37 36 csbeq1d 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = [_ O / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) )
38 1 fvexi 
 |-  B e. _V
39 4 38 rabex2 
 |-  O e. _V
40 39 a1i 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> O e. _V )
41 simplrr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> g = F )
42 41 rneqd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ran g = ran F )
43 simpr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> o = O )
44 42 43 sseq12d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( ran g C_ o <-> ran F C_ O ) )
45 11 adantr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> w = G )
46 45 fveq2d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( 0g ` w ) = ( 0g ` G ) )
47 46 2 eqtr4di 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( 0g ` w ) = .0. )
48 41 dmeqd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom g = dom F )
49 8 ad2antrr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom F = A )
50 48 49 eqtrd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom g = A )
51 50 eleq1d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( dom g e. ran ... <-> A e. ran ... ) )
52 50 eqeq1d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( dom g = ( m ... n ) <-> A = ( m ... n ) ) )
53 15 adantr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( +g ` w ) = .+ )
54 53 seqeq2d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( ( +g ` w ) , g ) = seq m ( .+ , g ) )
55 41 seqeq3d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( .+ , g ) = seq m ( .+ , F ) )
56 54 55 eqtrd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( ( +g ` w ) , g ) = seq m ( .+ , F ) )
57 56 fveq1d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( seq m ( ( +g ` w ) , g ) ` n ) = ( seq m ( .+ , F ) ` n ) )
58 57 eqeq2d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( x = ( seq m ( ( +g ` w ) , g ) ` n ) <-> x = ( seq m ( .+ , F ) ` n ) ) )
59 52 58 anbi12d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) <-> ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) )
60 59 rexbidv 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) <-> E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) )
61 60 exbidv 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) <-> E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) )
62 61 iotabidv 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) = ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) )
63 43 difeq2d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( _V \ o ) = ( _V \ O ) )
64 63 imaeq2d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' F " ( _V \ o ) ) = ( `' F " ( _V \ O ) ) )
65 41 cnveqd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> `' g = `' F )
66 65 imaeq1d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' g " ( _V \ o ) ) = ( `' F " ( _V \ o ) ) )
67 5 ad2antrr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> W = ( `' F " ( _V \ O ) ) )
68 64 66 67 3eqtr4d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' g " ( _V \ o ) ) = W )
69 68 sbceq1d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> [. W / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) )
70 cnvexg 
 |-  ( F e. X -> `' F e. _V )
71 imaexg 
 |-  ( `' F e. _V -> ( `' F " ( _V \ O ) ) e. _V )
72 7 70 71 3syl 
 |-  ( ph -> ( `' F " ( _V \ O ) ) e. _V )
73 5 72 eqeltrd 
 |-  ( ph -> W e. _V )
74 73 ad2antrr 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> W e. _V )
75 fveq2 
 |-  ( y = W -> ( # ` y ) = ( # ` W ) )
76 75 adantl 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( # ` y ) = ( # ` W ) )
77 76 oveq2d 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( 1 ... ( # ` y ) ) = ( 1 ... ( # ` W ) ) )
78 77 f1oeq2d 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> y ) )
79 f1oeq3 
 |-  ( y = W -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
80 79 adantl 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
81 78 80 bitrd 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
82 53 seqeq2d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( g o. f ) ) )
83 41 coeq1d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( g o. f ) = ( F o. f ) )
84 83 seqeq3d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( .+ , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) )
85 82 84 eqtrd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) )
86 85 adantr 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) )
87 86 76 fveq12d 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
88 87 eqeq2d 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) <-> x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) )
89 81 88 anbi12d 
 |-  ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
90 74 89 sbcied 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( [. W / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
91 69 90 bitrd 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
92 91 exbidv 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
93 92 iotabidv 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) )
94 51 62 93 ifbieq12d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) = if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) )
95 44 47 94 ifbieq12d 
 |-  ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )
96 40 95 csbied 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> [_ O / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )
97 37 96 eqtrd 
 |-  ( ( ph /\ ( w = G /\ g = F ) ) -> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )
98 6 elexd 
 |-  ( ph -> G e. _V )
99 7 elexd 
 |-  ( ph -> F e. _V )
100 2 fvexi 
 |-  .0. e. _V
101 iotaex 
 |-  ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) e. _V
102 iotaex 
 |-  ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) e. _V
103 101 102 ifex 
 |-  if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) e. _V
104 100 103 ifex 
 |-  if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) e. _V
105 104 a1i 
 |-  ( ph -> if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) e. _V )
106 10 97 98 99 105 ovmpod 
 |-  ( ph -> ( G gsum F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) )