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