Theorem psrval 15050

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   f, 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( y, 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 15047	. . . 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 9	. . 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 535	. . . . . . . 8 |- ( ( ph /\ ( i = I /\ r = R ) ) -> i = I )
5	4	oveq2d 6101	. . . . . . 7 |- ( ( ph /\ ( i = I /\ r = R ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
6	5	rabeqdv 2815	. . . . . 6 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
7		psrval.d	. . . . . 6 |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
8	6, 7	eqtr4di 2289	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
9	8	csbeq1d 3154	. . . 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 ) } ) ) >. } ) )
10		nn0ex 9569	. . . . . . . . 9 |- NN0 e. _V
11		vex 2824	. . . . . . . . 9 |- i e. _V
12	10, 11	mapval 6934	. . . . . . . 8 |- ( NN0 ^m i ) = { f | f : i --> NN0 }
13		mapex 6928	. . . . . . . . 9 |- ( ( i e. _V /\ NN0 e. _V ) -> { f | f : i --> NN0 } e. _V )
14	11, 10, 13	mp2an 430	. . . . . . . 8 |- { f | f : i --> NN0 } e. _V
15	12, 14	eqeltri 2311	. . . . . . 7 |- ( NN0 ^m i ) e. _V
16	15	rabex 4280	. . . . . 6 |- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
17	8, 16	eqeltrrdi 2330	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> D e. _V )
18		simplrr 542	. . . . . . . . . . 11 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> r = R )
19	18	fveq2d 5699	. . . . . . . . . 10 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = ( Base ` R ) )
20		psrval.k	. . . . . . . . . 10 |- K = ( Base ` R )
21	19, 20	eqtr4di 2289	. . . . . . . . 9 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = K )
22		simpr 110	. . . . . . . . 9 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> d = D )
23	21, 22	oveq12d 6103	. . . . . . . 8 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = ( K ^m D ) )
24		psrval.b	. . . . . . . . 9 |- ( ph -> B = ( K ^m D ) )
25	24	ad2antrr 492	. . . . . . . 8 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B = ( K ^m D ) )
26	23, 25	eqtr4d 2274	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = B )
27	26	csbeq1d 3154	. . . . . 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 ) } ) ) >. } ) )
28		basfn 13411	. . . . . . . . . . 11 |- Base Fn _V
29		vex 2824	. . . . . . . . . . 11 |- r e. _V
30		funfvex 5712	. . . . . . . . . . . 12 |- ( ( Fun Base /\ r e. dom Base ) -> ( Base ` r ) e. _V )
31	30	funfni 5483	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ r e. _V ) -> ( Base ` r ) e. _V )
32	28, 29, 31	mp2an 430	. . . . . . . . . 10 |- ( Base ` r ) e. _V
33		vex 2824	. . . . . . . . . 10 |- d e. _V
34	32, 33	mapval 6934	. . . . . . . . 9 |- ( ( Base ` r ) ^m d ) = { f | f : d --> ( Base ` r ) }
35		mapex 6928	. . . . . . . . . 10 |- ( ( d e. _V /\ ( Base ` r ) e. _V ) -> { f | f : d --> ( Base ` r ) } e. _V )
36	33, 32, 35	mp2an 430	. . . . . . . . 9 |- { f | f : d --> ( Base ` r ) } e. _V
37	34, 36	eqeltri 2311	. . . . . . . 8 |- ( ( Base ` r ) ^m d ) e. _V
38	26, 37	eqeltrrdi 2330	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B e. _V )
39		simpr 110	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> b = B )
40	39	opeq2d 3911	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
41	18	adantr 276	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> r = R )
42	41	fveq2d 5699	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
43		psrval.a	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
44	42, 43	eqtr4di 2289	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = .+ )
45	44	ofeqd 6304	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
46	39, 39	xpeq12d 4799	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
47	45, 46	reseq12d 5064	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = ( oF .+ |` ( B X. B ) ) )
48		psrval.p	. . . . . . . . . . 11 |- .+b = ( oF .+ |` ( B X. B ) )
49	47, 48	eqtr4di 2289	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = .+b )
50	49	opeq2d 3911	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. = <. ( +g ` ndx ) , .+b >. )
51	22	adantr 276	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> d = D )
52	51	rabeqdv 2815	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { y e. d | y oR <_ k } = { y e. D | y oR <_ k } )
53	41	fveq2d 5699	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = ( .r ` R ) )
54		psrval.m	. . . . . . . . . . . . . . . . 17 |- .x. = ( .r ` R )
55	53, 54	eqtr4di 2289	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = .x. )
56	55	oveqd 6102	. . . . . . . . . . . . . . 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 ) ) ) )
57	52, 56	mpteq12dv 4213	. . . . . . . . . . . . . 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 ) ) ) ) )
58	41, 57	oveq12d 6103	. . . . . . . . . . . . 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 ) ) ) ) ) )
59	51, 58	mpteq12dv 4213	. . . . . . . . . . . 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 ) ) ) ) ) ) )
60	39, 39, 59	mpoeq123dv 6150	. . . . . . . . . . 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 ) ) ) ) ) ) ) )
61		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 ) ) ) ) ) ) )
62	60, 61	eqtr4di 2289	. . . . . . . . . 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. )
63	62	opeq2d 3911	. . . . . . . . 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. >. )
64	40, 50, 63	tpeq123d 3803	. . . . . . . 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. >. } )
65	41	opeq2d 3911	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. (Scalar ` ndx ) , r >. = <. (Scalar ` ndx ) , R >. )
66	21	adantr 276	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Base ` r ) = K )
67	55	ofeqd 6304	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
68	51	xpeq1d 4797	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { x } ) = ( D X. { x } ) )
69		eqidd 2239	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> f = f )
70	67, 68, 69	oveq123d 6106	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( ( d X. { x } ) oF ( .r ` r ) f ) = ( ( D X. { x } ) oF .x. f ) )
71	66, 39, 70	mpoeq123dv 6150	. . . . . . . . . . 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 ) ) )
72		psrval.v	. . . . . . . . . . 11 |- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
73	71, 72	eqtr4di 2289	. . . . . . . . . 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 )
74	73	opeq2d 3911	. . . . . . . . 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 >. )
75	41	fveq2d 5699	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = ( TopOpen ` R ) )
76		psrval.o	. . . . . . . . . . . . . . 15 |- O = ( TopOpen ` R )
77	75, 76	eqtr4di 2289	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = O )
78	77	sneqd 3722	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
79	51, 78	xpeq12d 4799	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
80	79	fveq2d 5699	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = ( Xt_ ` ( D X. { O } ) ) )
81		psrval.j	. . . . . . . . . . . 12 |- ( ph -> J = ( Xt_ ` ( D X. { O } ) ) )
82	81	ad3antrrr 496	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> J = ( Xt_ ` ( D X. { O } ) ) )
83	80, 82	eqtr4d 2274	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = J )
84	83	opeq2d 3911	. . . . . . . . 9 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. = <. (TopSet ` ndx ) , J >. )
85	65, 74, 84	tpeq123d 3803	. . . . . . . 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 >. } )
86	64, 85	uneq12d 3384	. . . . . . 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 >. } ) )
87	38, 86	csbied 3194	. . . . . 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 >. } ) )
88	27, 87	eqtrd 2271	. . . . 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 >. } ) )
89	17, 88	csbied 3194	. . . 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 >. } ) )
90	9, 89	eqtrd 2271	. . 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 >. } ) )
91		psrval.i	. . . 4 |- ( ph -> I e. W )
92	91	elexd 2835	. . 3 |- ( ph -> I e. _V )
93		psrval.r	. . . 4 |- ( ph -> R e. X )
94	93	elexd 2835	. . 3 |- ( ph -> R e. _V )
95		basendxnn 13408	. . . . . 6 |- ( Base ` ndx ) e. NN
96		funfvex 5712	. . . . . . . . . . . 12 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
97	96	funfni 5483	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ R e. _V ) -> ( Base ` R ) e. _V )
98	28, 94, 97	sylancr 418	. . . . . . . . . 10 |- ( ph -> ( Base ` R ) e. _V )
99	20, 98	eqeltrid 2325	. . . . . . . . 9 |- ( ph -> K e. _V )
100		mapvalg 6932	. . . . . . . . . . . . 13 |- ( ( NN0 e. _V /\ I e. W ) -> ( NN0 ^m I ) = { f | f : I --> NN0 } )
101	10, 91, 100	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( NN0 ^m I ) = { f | f : I --> NN0 } )
102		mapex 6928	. . . . . . . . . . . . 13 |- ( ( I e. W /\ NN0 e. _V ) -> { f | f : I --> NN0 } e. _V )
103	91, 10, 102	sylancl 417	. . . . . . . . . . . 12 |- ( ph -> { f | f : I --> NN0 } e. _V )
104	101, 103	eqeltrd 2315	. . . . . . . . . . 11 |- ( ph -> ( NN0 ^m I ) e. _V )
105		rabexg 4279	. . . . . . . . . . 11 |- ( ( NN0 ^m I ) e. _V -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
106	104, 105	syl 14	. . . . . . . . . 10 |- ( ph -> { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } e. _V )
107	7, 106	eqeltrid 2325	. . . . . . . . 9 |- ( ph -> D e. _V )
108		mapvalg 6932	. . . . . . . . 9 |- ( ( K e. _V /\ D e. _V ) -> ( K ^m D ) = { f | f : D --> K } )
109	99, 107, 108	syl2anc 415	. . . . . . . 8 |- ( ph -> ( K ^m D ) = { f | f : D --> K } )
110		mapex 6928	. . . . . . . . 9 |- ( ( D e. _V /\ K e. _V ) -> { f | f : D --> K } e. _V )
111	107, 99, 110	syl2anc 415	. . . . . . . 8 |- ( ph -> { f | f : D --> K } e. _V )
112	109, 111	eqeltrd 2315	. . . . . . 7 |- ( ph -> ( K ^m D ) e. _V )
113	24, 112	eqeltrd 2315	. . . . . 6 |- ( ph -> B e. _V )
114		opexg 4368	. . . . . 6 |- ( ( ( Base ` ndx ) e. NN /\ B e. _V ) -> <. ( Base ` ndx ) , B >. e. _V )
115	95, 113, 114	sylancr 418	. . . . 5 |- ( ph -> <. ( Base ` ndx ) , B >. e. _V )
116		plusgndxnn 13465	. . . . . 6 |- ( +g ` ndx ) e. NN
117	113, 113	ofmresex 6370	. . . . . . 7 |- ( ph -> ( oF .+ |` ( B X. B ) ) e. _V )
118	48, 117	eqeltrid 2325	. . . . . 6 |- ( ph -> .+b e. _V )
119		opexg 4368	. . . . . 6 |- ( ( ( +g ` ndx ) e. NN /\ .+b e. _V ) -> <. ( +g ` ndx ) , .+b >. e. _V )
120	116, 118, 119	sylancr 418	. . . . 5 |- ( ph -> <. ( +g ` ndx ) , .+b >. e. _V )
121		mulrslid 13486	. . . . . . 7 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
122	121	simpri 113	. . . . . 6 |- ( .r ` ndx ) e. NN
123	61	mpoexg 6447	. . . . . . 7 |- ( ( B e. _V /\ B e. _V ) -> .X. e. _V )
124	113, 113, 123	syl2anc 415	. . . . . 6 |- ( ph -> .X. e. _V )
125		opexg 4368	. . . . . 6 |- ( ( ( .r ` ndx ) e. NN /\ .X. e. _V ) -> <. ( .r ` ndx ) , .X. >. e. _V )
126	122, 124, 125	sylancr 418	. . . . 5 |- ( ph -> <. ( .r ` ndx ) , .X. >. e. _V )
127		tpexg 4590	. . . . 5 |- ( ( <. ( Base ` ndx ) , B >. e. _V /\ <. ( +g ` ndx ) , .+b >. e. _V /\ <. ( .r ` ndx ) , .X. >. e. _V ) -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V )
128	115, 120, 126, 127	syl3anc 1278	. . . 4 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V )
129		scaslid 13507	. . . . . . 7 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
130	129	simpri 113	. . . . . 6 |- (Scalar ` ndx ) e. NN
131		opexg 4368	. . . . . 6 |- ( ( (Scalar ` ndx ) e. NN /\ R e. X ) -> <. (Scalar ` ndx ) , R >. e. _V )
132	130, 93, 131	sylancr 418	. . . . 5 |- ( ph -> <. (Scalar ` ndx ) , R >. e. _V )
133		vscaslid 13517	. . . . . . 7 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
134	133	simpri 113	. . . . . 6 |- ( .s ` ndx ) e. NN
135	72	mpoexg 6447	. . . . . . 7 |- ( ( K e. _V /\ B e. _V ) -> .xb e. _V )
136	99, 113, 135	syl2anc 415	. . . . . 6 |- ( ph -> .xb e. _V )
137		opexg 4368	. . . . . 6 |- ( ( ( .s ` ndx ) e. NN /\ .xb e. _V ) -> <. ( .s ` ndx ) , .xb >. e. _V )
138	134, 136, 137	sylancr 418	. . . . 5 |- ( ph -> <. ( .s ` ndx ) , .xb >. e. _V )
139		tsetndxnn 13543	. . . . . 6 |- (TopSet ` ndx ) e. NN
140		topnfn 13598	. . . . . . . . . . . 12 |- TopOpen Fn _V
141		funfvex 5712	. . . . . . . . . . . . 13 |- ( ( Fun TopOpen /\ R e. dom TopOpen ) -> ( TopOpen ` R ) e. _V )
142	141	funfni 5483	. . . . . . . . . . . 12 |- ( ( TopOpen Fn _V /\ R e. _V ) -> ( TopOpen ` R ) e. _V )
143	140, 94, 142	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( TopOpen ` R ) e. _V )
144	76, 143	eqeltrid 2325	. . . . . . . . . 10 |- ( ph -> O e. _V )
145		snexg 4321	. . . . . . . . . 10 |- ( O e. _V -> { O } e. _V )
146	144, 145	syl 14	. . . . . . . . 9 |- ( ph -> { O } e. _V )
147		xpexg 4889	. . . . . . . . 9 |- ( ( D e. _V /\ { O } e. _V ) -> ( D X. { O } ) e. _V )
148	107, 146, 147	syl2anc 415	. . . . . . . 8 |- ( ph -> ( D X. { O } ) e. _V )
149		ptex 13618	. . . . . . . 8 |- ( ( D X. { O } ) e. _V -> ( Xt_ ` ( D X. { O } ) ) e. _V )
150	148, 149	syl 14	. . . . . . 7 |- ( ph -> ( Xt_ ` ( D X. { O } ) ) e. _V )
151	81, 150	eqeltrd 2315	. . . . . 6 |- ( ph -> J e. _V )
152		opexg 4368	. . . . . 6 |- ( ( (TopSet ` ndx ) e. NN /\ J e. _V ) -> <. (TopSet ` ndx ) , J >. e. _V )
153	139, 151, 152	sylancr 418	. . . . 5 |- ( ph -> <. (TopSet ` ndx ) , J >. e. _V )
154		tpexg 4590	. . . . 5 |- ( ( <. (Scalar ` ndx ) , R >. e. _V /\ <. ( .s ` ndx ) , .xb >. e. _V /\ <. (TopSet ` ndx ) , J >. e. _V ) -> { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } e. _V )
155	132, 138, 153, 154	syl3anc 1278	. . . 4 |- ( ph -> { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } e. _V )
156		unexg 4589	. . . 4 |- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V /\ { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } e. _V ) -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) e. _V )
157	128, 155, 156	syl2anc 415	. . 3 |- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) e. _V )
158	3, 90, 92, 94, 157	ovmpod 6216	. 2 |- ( ph -> ( I mPwSer R ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
159	1, 158	eqtrid 2283	1 |- ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   {cab 2224   {crab 2532   _Vcvv 2821   [_csb 3147   u. cun 3218   {csn 3709   {ctp 3711   <.cop 3712   class class class wbr 4130   |-> cmpt 4192   X. cxp 4772   `'ccnv 4773   |` cres 4776   "cima 4777   Fn wfn 5372   -->wf 5373   ` cfv 5377  (class class class)co 6085   e. cmpo 6087   oFcof 6300   oRcofr 6301   ^m cmap 6922   Fincfn 7022   <_ cle 8361   - cmin 8497   NNcn 9304   NN0cn0 9563   ndxcnx 13349  Slot cslot 13351   Basecbs 13352   +g cplusg 13431   .rcmulr 13432  Scalarcsca 13434   .scvsca 13435  TopSetcts 13437   TopOpenctopn 13594   Xt_cpt 13609   gsum_g cgsu 14150   mPwSer cmps 15045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-cnex 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-i2m1 8284

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-tp 3717  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-of 6302  df-1st 6374  df-2nd 6375  df-map 6924  df-ixp 6981  df-inn 9305  df-2 9363  df-3 9364  df-4 9365  df-5 9366  df-6 9367  df-7 9368  df-8 9369  df-9 9370  df-n0 9564  df-ndx 13355  df-slot 13356  df-base 13358  df-plusg 13444  df-mulr 13445  df-sca 13447  df-vsca 13448  df-tset 13450  df-rest 13595  df-topn 13596  df-topgen 13614  df-pt 13615  df-psr 15047

This theorem is used by:  psrbasg  15065  psrplusgg  15069