Theorem gsumvalx 17270

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

Hypotheses

Ref	Expression
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

Ref	Expression
gsumvalx	|- ( ph -> ( G gsumg 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 ) ) ) ) ) ) )

Distinct variable groups:   t, s, x, B   f, m, n, x, ph   f, F, m, n, x   f, G, m, n, x   .+ , s, t, x   f, O, m, n, x

Allowed substitution hints:   ph( t, s)   A( x, t, f, m, n, s)   B( f, m, n)   .+ ( f, m, n)   F( t, s)   G( t, s)   O( t, s)   V( x, t, f, m, n, s)   W( x, t, f, m, n, s)   X( x, t, f, m, n, s)   .0. ( x, t, f, m, n, s)

Proof of Theorem gsumvalx

Dummy variables g o w y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-gsum 16103	. . 3 |- gsumg = ( 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 ) ) ) ) ) ) )
2	1	a1i 11	. 2 |- ( ph -> gsumg = ( 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 ) ) ) ) ) ) ) )
3		simprl 794	. . . . . . . 8 |- ( ( ph /\ ( w = G /\ g = F ) ) -> w = G )
4	3	fveq2d 6195	. . . . . . 7 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( Base ` w ) = ( Base ` G ) )
5		gsumval.b	. . . . . . 7 |- B = ( Base ` G )
6	4, 5	syl6eqr 2674	. . . . . 6 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( Base ` w ) = B )
7	3	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( +g ` w ) = ( +g ` G ) )
8		gsumval.p	. . . . . . . . . . 11 |- .+ = ( +g ` G )
9	7, 8	syl6eqr 2674	. . . . . . . . . 10 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( +g ` w ) = .+ )
10	9	oveqd 6667	. . . . . . . . 9 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( x ( +g ` w ) y ) = ( x .+ y ) )
11	10	eqeq1d 2624	. . . . . . . 8 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( x ( +g ` w ) y ) = y <-> ( x .+ y ) = y ) )
12	9	oveqd 6667	. . . . . . . . 9 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( y ( +g ` w ) x ) = ( y .+ x ) )
13	12	eqeq1d 2624	. . . . . . . 8 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( y ( +g ` w ) x ) = y <-> ( y .+ x ) = y ) )
14	11, 13	anbi12d 747	. . . . . . 7 |- ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) <-> ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
15	6, 14	raleqbidv 3152	. . . . . 6 |- ( ( 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 ) ) )
16	6, 15	rabeqbidv 3195	. . . . 5 |- ( ( 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 ) } )
17		gsumval.o	. . . . . 6 |- O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) }
18		oveq2 6658	. . . . . . . . . . 11 |- ( t = y -> ( s .+ t ) = ( s .+ y ) )
19		id 22	. . . . . . . . . . 11 |- ( t = y -> t = y )
20	18, 19	eqeq12d 2637	. . . . . . . . . 10 |- ( t = y -> ( ( s .+ t ) = t <-> ( s .+ y ) = y ) )
21		oveq1 6657	. . . . . . . . . . 11 |- ( t = y -> ( t .+ s ) = ( y .+ s ) )
22	21, 19	eqeq12d 2637	. . . . . . . . . 10 |- ( t = y -> ( ( t .+ s ) = t <-> ( y .+ s ) = y ) )
23	20, 22	anbi12d 747	. . . . . . . . 9 |- ( t = y -> ( ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> ( ( s .+ y ) = y /\ ( y .+ s ) = y ) ) )
24	23	cbvralv 3171	. . . . . . . 8 |- ( A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> A. y e. B ( ( s .+ y ) = y /\ ( y .+ s ) = y ) )
25		oveq1 6657	. . . . . . . . . . 11 |- ( s = x -> ( s .+ y ) = ( x .+ y ) )
26	25	eqeq1d 2624	. . . . . . . . . 10 |- ( s = x -> ( ( s .+ y ) = y <-> ( x .+ y ) = y ) )
27		oveq2 6658	. . . . . . . . . . 11 |- ( s = x -> ( y .+ s ) = ( y .+ x ) )
28	27	eqeq1d 2624	. . . . . . . . . 10 |- ( s = x -> ( ( y .+ s ) = y <-> ( y .+ x ) = y ) )
29	26, 28	anbi12d 747	. . . . . . . . 9 |- ( s = x -> ( ( ( s .+ y ) = y /\ ( y .+ s ) = y ) <-> ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
30	29	ralbidv 2986	. . . . . . . 8 |- ( s = x -> ( A. y e. B ( ( s .+ y ) = y /\ ( y .+ s ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
31	24, 30	syl5bb 272	. . . . . . 7 |- ( s = x -> ( A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
32	31	cbvrabv 3199	. . . . . 6 |- { 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 ) }
33	17, 32	eqtri 2644	. . . . 5 |- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
34	16, 33	syl6eqr 2674	. . . 4 |- ( ( 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 )
35	34	csbeq1d 3540	. . 3 |- ( ( 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 ) ) ) ) ) ) )
36		fvex 6201	. . . . . . 7 |- ( Base ` G ) e. _V
37	5, 36	eqeltri 2697	. . . . . 6 |- B e. _V
38	17, 37	rabex2 4815	. . . . 5 |- O e. _V
39	38	a1i 11	. . . 4 |- ( ( ph /\ ( w = G /\ g = F ) ) -> O e. _V )
40		simplrr 801	. . . . . . 7 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> g = F )
41	40	rneqd 5353	. . . . . 6 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ran g = ran F )
42		simpr 477	. . . . . 6 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> o = O )
43	41, 42	sseq12d 3634	. . . . 5 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( ran g C_ o <-> ran F C_ O ) )
44	3	adantr 481	. . . . . . 7 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> w = G )
45	44	fveq2d 6195	. . . . . 6 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( 0g ` w ) = ( 0g ` G ) )
46		gsumval.z	. . . . . 6 |- .0. = ( 0g ` G )
47	45, 46	syl6eqr 2674	. . . . 5 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( 0g ` w ) = .0. )
48	40	dmeqd 5326	. . . . . . . 8 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom g = dom F )
49		gsumvalx.a	. . . . . . . . 9 |- ( ph -> dom F = A )
50	49	ad2antrr 762	. . . . . . . 8 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom F = A )
51	48, 50	eqtrd 2656	. . . . . . 7 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom g = A )
52	51	eleq1d 2686	. . . . . 6 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( dom g e. ran ... <-> A e. ran ... ) )
53	51	eqeq1d 2624	. . . . . . . . . 10 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( dom g = ( m ... n ) <-> A = ( m ... n ) ) )
54	9	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( +g ` w ) = .+ )
55	54	seqeq2d 12808	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( ( +g ` w ) , g ) = seq m ( .+ , g ) )
56	40	seqeq3d 12809	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( .+ , g ) = seq m ( .+ , F ) )
57	55, 56	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( ( +g ` w ) , g ) = seq m ( .+ , F ) )
58	57	fveq1d 6193	. . . . . . . . . . 11 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( seq m ( ( +g ` w ) , g ) ` n ) = ( seq m ( .+ , F ) ` n ) )
59	58	eqeq2d 2632	. . . . . . . . . 10 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( x = ( seq m ( ( +g ` w ) , g ) ` n ) <-> x = ( seq m ( .+ , F ) ` n ) ) )
60	53, 59	anbi12d 747	. . . . . . . . 9 |- ( ( ( 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 ) ) ) )
61	60	rexbidv 3052	. . . . . . . 8 |- ( ( ( 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 ) ) ) )
62	61	exbidv 1850	. . . . . . 7 |- ( ( ( 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 ) ) ) )
63	62	iotabidv 5872	. . . . . 6 |- ( ( ( 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 ) ) ) )
64	42	difeq2d 3728	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( _V \ o ) = ( _V \ O ) )
65	64	imaeq2d 5466	. . . . . . . . . . 11 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' F " ( _V \ o ) ) = ( `' F " ( _V \ O ) ) )
66	40	cnveqd 5298	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> `' g = `' F )
67	66	imaeq1d 5465	. . . . . . . . . . 11 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' g " ( _V \ o ) ) = ( `' F " ( _V \ o ) ) )
68		gsumval.w	. . . . . . . . . . . 12 |- ( ph -> W = ( `' F " ( _V \ O ) ) )
69	68	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> W = ( `' F " ( _V \ O ) ) )
70	65, 67, 69	3eqtr4d 2666	. . . . . . . . . 10 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' g " ( _V \ o ) ) = W )
71	70	sbceq1d 3440	. . . . . . . . 9 |- ( ( ( 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 ) ) ) ) )
72		gsumvalx.f	. . . . . . . . . . . . 13 |- ( ph -> F e. X )
73		cnvexg 7112	. . . . . . . . . . . . 13 |- ( F e. X -> `' F e. _V )
74		imaexg 7103	. . . . . . . . . . . . 13 |- ( `' F e. _V -> ( `' F " ( _V \ O ) ) e. _V )
75	72, 73, 74	3syl 18	. . . . . . . . . . . 12 |- ( ph -> ( `' F " ( _V \ O ) ) e. _V )
76	68, 75	eqeltrd 2701	. . . . . . . . . . 11 |- ( ph -> W e. _V )
77	76	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> W e. _V )
78		fveq2 6191	. . . . . . . . . . . . . . 15 |- ( y = W -> ( # ` y ) = ( # ` W ) )
79	78	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( # ` y ) = ( # ` W ) )
80	79	oveq2d 6666	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( 1 ... ( # ` y ) ) = ( 1 ... ( # ` W ) ) )
81		f1oeq2 6128	. . . . . . . . . . . . 13 |- ( ( 1 ... ( # ` y ) ) = ( 1 ... ( # ` W ) ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> y ) )
82	80, 81	syl 17	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> y ) )
83		f1oeq3 6129	. . . . . . . . . . . . 13 |- ( y = W -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
84	83	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
85	82, 84	bitrd 268	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) )
86	54	seqeq2d 12808	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( g o. f ) ) )
87	40	coeq1d 5283	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( g o. f ) = ( F o. f ) )
88	87	seqeq3d 12809	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( .+ , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) )
89	86, 88	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) )
90	89	adantr 481	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) )
91	90, 79	fveq12d 6197	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) )
92	91	eqeq2d 2632	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
93	85, 92	anbi12d 747	. . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) ) )
94	77, 93	sbcied 3472	. . . . . . . . 9 |- ( ( ( 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 ) ) ) ) )
95	71, 94	bitrd 268	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) )
96	95	exbidv 1850	. . . . . . 7 |- ( ( ( 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 ) ) ) ) )
97	96	iotabidv 5872	. . . . . 6 |- ( ( ( 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 ) ) ) ) )
98	52, 63, 97	ifbieq12d 4113	. . . . 5 |- ( ( ( 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 ) ) ) ) ) )
99	43, 47, 98	ifbieq12d 4113	. . . 4 |- ( ( ( 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 ) ) ) ) ) ) )
100	39, 99	csbied 3560	. . 3 |- ( ( 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 ) ) ) ) ) ) )
101	35, 100	eqtrd 2656	. 2 |- ( ( 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 ) ) ) ) ) ) )
102		gsumval.g	. . 3 |- ( ph -> G e. V )
103	102	elexd 3214	. 2 |- ( ph -> G e. _V )
104	72	elexd 3214	. 2 |- ( ph -> F e. _V )
105		fvex 6201	. . . . 5 |- ( 0g ` G ) e. _V
106	46, 105	eqeltri 2697	. . . 4 |- .0. e. _V
107		iotaex 5868	. . . . 5 |- ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) e. _V
108		iotaex 5868	. . . . 5 |- ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) e. _V
109	107, 108	ifex 4156	. . . 4 |- 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
110	106, 109	ifex 4156	. . 3 |- 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
111	110	a1i 11	. 2 |- ( 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 )
112	2, 101, 103, 104, 111	ovmpt2d 6788	1 |- ( ph -> ( G gsumg 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 ) ) ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [.wsbc 3435   [_csb 3533   \ cdif 3571   C_ wss 3574   ifcif 4086   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   o. ccom 5118   iotacio 5849   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   1c1 9937   ZZ>=cuz 11687   ...cfz 12326   seqcseq 12801   #chash 13117   Basecbs 15857   +g cplusg 15941   0gc0g 16100   gsum_g cgsu 16101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-seq 12802  df-gsum 16103

This theorem is referenced by:  gsumval  17271  gsumpropd  17272  gsumpropd2lem  17273