Theorem psrval 17544

Description: Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.)

Hypotheses

Ref	Expression
psrval.s	|- S = ( I mPwSer R )
psrval.k	|- K = ( Base ` R )
psrval.a	|- .+ = ( +g ` R )
psrval.m	|- .x. = ( .r ` R )
psrval.o	|- O = ( TopOpen ` R )
psrval.d	|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
psrval.b	|- ( ph -> B = ( K ^m D ) )
psrval.p	|- .+b = ( oF .+ |` ( B X. B ) )
psrval.t	|- .X. = ( f e. B , g e. B |-> ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
psrval.v	|- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
psrval.j	|- ( ph -> J = ( Xt_ ` ( D X. { O } ) ) )
psrval.i	|- ( ph -> I e. W )
psrval.r	|- ( ph -> R e. X )

Assertion

Ref	Expression
psrval	|- ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )

Distinct variable groups:   y, h   f, g, k, x, ph   B, f, g, k, x   f, h, I, g, k, x   R, f, g, k, x   y, f, D, g, k, x

Allowed substitution hints:   ph( y, h)   B( y, h)   D( h)   .+ ( x, y, f, g, h, k)   .+b ( x, y, f, g, h, k)   R( y, h)   S( x, y, f, g, h, k)   .xb ( x, y, f, g, h, k)   .x. ( x, y, f, g, h, k)   .X. ( x, y, f, g, h, k)   I( y)   J( x, y, f, g, h, k)   K( x, y, f, g, h, k)   O( x, y, f, g, h, k)   W( x, y, f, g, h, k)   X( x, y, f, g, h, k)

Proof of Theorem psrval

Dummy variables i r b d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psrval.s	. 2 |- S = ( I mPwSer R )
2		df-psr 17538	. . . 4 |- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
3	2	a1i 11	. . 3 |- ( ph -> mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) ) )
4		simprl 755	. . . . . . . 8 |- ( ( ph /\ ( i = I /\ r = R ) ) -> i = I )
5	4	oveq2d 6209	. . . . . . 7 |- ( ( ph /\ ( i = I /\ r = R ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
6		rabeq 3065	. . . . . . 7 |- ( ( NN0 ^m i ) = ( NN0 ^m I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
7	5, 6	syl 16	. . . . . 6 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
8		psrval.d	. . . . . 6 |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
9	7, 8	syl6eqr 2510	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
10	9	csbeq1d 3396	. . . 4 |- ( ( ph /\ ( i = I /\ r = R ) ) -> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = [_ D / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
11		ovex 6218	. . . . . . 7 |- ( NN0 ^m i ) e. _V
12	11	rabex 4544	. . . . . 6 |- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
13	9, 12	syl6eqelr 2548	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> D e. _V )
14		simplrr 760	. . . . . . . . . . 11 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> r = R )
15	14	fveq2d 5796	. . . . . . . . . 10 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = ( Base ` R ) )
16		psrval.k	. . . . . . . . . 10 |- K = ( Base ` R )
17	15, 16	syl6eqr 2510	. . . . . . . . 9 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = K )
18		simpr 461	. . . . . . . . 9 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> d = D )
19	17, 18	oveq12d 6211	. . . . . . . 8 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = ( K ^m D ) )
20		psrval.b	. . . . . . . . 9 |- ( ph -> B = ( K ^m D ) )
21	20	ad2antrr 725	. . . . . . . 8 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B = ( K ^m D ) )
22	19, 21	eqtr4d 2495	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = B )
23	22	csbeq1d 3396	. . . . . 6 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = [_ B / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
24		ovex 6218	. . . . . . . 8 |- ( ( Base ` r ) ^m d ) e. _V
25	22, 24	syl6eqelr 2548	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B e. _V )
26		simpr 461	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> b = B )
27	26	opeq2d 4167	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
28	14	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> r = R )
29	28	fveq2d 5796	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
30		psrval.a	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
31	29, 30	syl6eqr 2510	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = .+ )
32		ofeq 6425	. . . . . . . . . . . . 13 |- ( ( +g ` r ) = .+ -> oF ( +g ` r ) = oF .+ )
33	31, 32	syl 16	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
34	26, 26	xpeq12d 4966	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
35	33, 34	reseq12d 5212	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = ( oF .+ |` ( B X. B ) ) )
36		psrval.p	. . . . . . . . . . 11 |- .+b = ( oF .+ |` ( B X. B ) )
37	35, 36	syl6eqr 2510	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = .+b )
38	37	opeq2d 4167	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. = <. ( +g ` ndx ) , .+b >. )
39	18	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> d = D )
40		rabeq 3065	. . . . . . . . . . . . . . . 16 |- ( d = D -> { y e. d | y oR <_ k } = { y e. D | y oR <_ k } )
41	39, 40	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { y e. d | y oR <_ k } = { y e. D | y oR <_ k } )
42	28	fveq2d 5796	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = ( .r ` R ) )
43		psrval.m	. . . . . . . . . . . . . . . . 17 |- .x. = ( .r ` R )
44	42, 43	syl6eqr 2510	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = .x. )
45	44	oveqd 6210	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) = ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) )
46	41, 45	mpteq12dv 4471	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) = ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) )
47	28, 46	oveq12d 6211	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) = ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) )
48	39, 47	mpteq12dv 4471	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) = ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
49	26, 26, 48	mpt2eq123dv 6250	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) = ( f e. B , g e. B |-> ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) )
50		psrval.t	. . . . . . . . . . 11 |- .X. = ( f e. B , g e. B |-> ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
51	49, 50	syl6eqr 2510	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) = .X. )
52	51	opeq2d 4167	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. = <. ( .r ` ndx ) , .X. >. )
53	27, 38, 52	tpeq123d 4070	. . . . . . . 8 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } )
54	28	opeq2d 4167	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. (Scalar ` ndx ) , r >. = <. (Scalar ` ndx ) , R >. )
55	17	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Base ` r ) = K )
56		ofeq 6425	. . . . . . . . . . . . . 14 |- ( ( .r ` r ) = .x. -> oF ( .r ` r ) = oF .x. )
57	44, 56	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
58	39	xpeq1d 4964	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { x } ) = ( D X. { x } ) )
59		eqidd 2452	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> f = f )
60	57, 58, 59	oveq123d 6214	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( ( d X. { x } ) oF ( .r ` r ) f ) = ( ( D X. { x } ) oF .x. f ) )
61	55, 26, 60	mpt2eq123dv 6250	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) )
62		psrval.v	. . . . . . . . . . 11 |- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
63	61, 62	syl6eqr 2510	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) = .xb )
64	63	opeq2d 4167	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. = <. ( .s ` ndx ) , .xb >. )
65	28	fveq2d 5796	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = ( TopOpen ` R ) )
66		psrval.o	. . . . . . . . . . . . . . 15 |- O = ( TopOpen ` R )
67	65, 66	syl6eqr 2510	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = O )
68	67	sneqd 3990	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
69	39, 68	xpeq12d 4966	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
70	69	fveq2d 5796	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = ( Xt_ ` ( D X. { O } ) ) )
71		psrval.j	. . . . . . . . . . . 12 |- ( ph -> J = ( Xt_ ` ( D X. { O } ) ) )
72	71	ad3antrrr 729	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> J = ( Xt_ ` ( D X. { O } ) ) )
73	70, 72	eqtr4d 2495	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = J )
74	73	opeq2d 4167	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. = <. (TopSet ` ndx ) , J >. )
75	54, 64, 74	tpeq123d 4070	. . . . . . . 8 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } = { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } )
76	53, 75	uneq12d 3612	. . . . . . 7 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
77	25, 76	csbied 3415	. . . . . 6 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> [_ B / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
78	23, 77	eqtrd 2492	. . . . 5 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
79	13, 78	csbied 3415	. . . 4 |- ( ( ph /\ ( i = I /\ r = R ) ) -> [_ D / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
80	10, 79	eqtrd 2492	. . 3 |- ( ( ph /\ ( i = I /\ r = R ) ) -> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
81		psrval.i	. . . 4 |- ( ph -> I e. W )
82		elex 3080	. . . 4 |- ( I e. W -> I e. _V )
83	81, 82	syl 16	. . 3 |- ( ph -> I e. _V )
84		psrval.r	. . . 4 |- ( ph -> R e. X )
85		elex 3080	. . . 4 |- ( R e. X -> R e. _V )
86	84, 85	syl 16	. . 3 |- ( ph -> R e. _V )
87		tpex 6482	. . . . 5 |- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V
88		tpex 6482	. . . . 5 |- { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } e. _V
89	87, 88	unex 6481	. . . 4 |- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) e. _V
90	89	a1i 11	. . 3 |- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) e. _V )
91	3, 80, 83, 86, 90	ovmpt2d 6321	. 2 |- ( ph -> ( I mPwSer R ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
92	1, 91	syl5eq 2504	1 |- ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   {crab 2799   _Vcvv 3071   [_csb 3389   u. cun 3427   {csn 3978   {ctp 3982   <.cop 3984   class class class wbr 4393   |-> cmpt 4451   X. cxp 4939   `'ccnv 4940   |` cres 4943   "cima 4944   ` cfv 5519  (class class class)co 6193   |-> cmpt2 6195   oFcof 6421   oRcofr 6422   ^m cmap 7317   Fincfn 7413   <_ cle 9523   - cmin 9699   NNcn 10426   NN0cn0 10683   ndxcnx 14282   Basecbs 14285   +g cplusg 14349   .rcmulr 14350  Scalarcsca 14352   .scvsca 14353  TopSetcts 14355   TopOpenctopn 14471   Xt_cpt 14488   gsum_g cgsu 14490   mPwSer cmps 17533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632  ax-un 6475

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-tp 3983  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-res 4953  df-iota 5482  df-fun 5521  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-of 6423  df-psr 17538

This theorem is referenced by:  psrbas  17563  psrbasOLD  17564  psrplusg  17567  psrmulr  17570  psrsca  17575  psrvscafval  17576