Theorem psrval 14973

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 14970	. . . 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 6091	. . . . . . 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 9548	. . . . . . . . 9 |- NN0 e. _V
11		vex 2824	. . . . . . . . 9 |- i e. _V
12	10, 11	mapval 6924	. . . . . . . 8 |- ( NN0 ^m i ) = { f | f : i --> NN0 }
13		mapex 6918	. . . . . . . . 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 4275	. . . . . 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 5694	. . . . . . . . . 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 6093	. . . . . . . 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 13389	. . . . . . . . . . 11 |- Base Fn _V
29		vex 2824	. . . . . . . . . . 11 |- r e. _V
30		funfvex 5707	. . . . . . . . . . . 12 |- ( ( Fun Base /\ r e. dom Base ) -> ( Base ` r ) e. _V )
31	30	funfni 5478	. . . . . . . . . . 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 6924	. . . . . . . . 9 |- ( ( Base ` r ) ^m d ) = { f | f : d --> ( Base ` r ) }
35		mapex 6918	. . . . . . . . . 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 3906	. . . . . . . . 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 5694	. . . . . . . . . . . . . 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 6294	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
46	39, 39	xpeq12d 4794	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
47	45, 46	reseq12d 5059	. . . . . . . . . . 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 3906	. . . . . . . . 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 5694	. . . . . . . . . . . . . . . . 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 6092	. . . . . . . . . . . . . . 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 4208	. . . . . . . . . . . . . 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 6093	. . . . . . . . . . . . 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 4208	. . . . . . . . . . . 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 6140	. . . . . . . . . . 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 3906	. . . . . . . . 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 3799	. . . . . . . 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 3906	. . . . . . . . 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 6294	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
68	51	xpeq1d 4792	. . . . . . . . . . . . 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 6096	. . . . . . . . . . . 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 6140	. . . . . . . . . . 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 3906	. . . . . . . . 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 5694	. . . . . . . . . . . . . . 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 3718	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
79	51, 78	xpeq12d 4794	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
80	79	fveq2d 5694	. . . . . . . . . . 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 3906	. . . . . . . . 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 3799	. . . . . . . 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 13386	. . . . . 6 |- ( Base ` ndx ) e. NN
96		funfvex 5707	. . . . . . . . . . . 12 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
97	96	funfni 5478	. . . . . . . . . . 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 6922	. . . . . . . . . . . . 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 6918	. . . . . . . . . . . . 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 4274	. . . . . . . . . . 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 6922	. . . . . . . . 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 6918	. . . . . . . . 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 4363	. . . . . 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 13442	. . . . . 6 |- ( +g ` ndx ) e. NN
117	113, 113	ofmresex 6360	. . . . . . 7 |- ( ph -> ( oF .+ |` ( B X. B ) ) e. _V )
118	48, 117	eqeltrid 2325	. . . . . 6 |- ( ph -> .+b e. _V )
119		opexg 4363	. . . . . 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 13463	. . . . . . 7 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
122	121	simpri 113	. . . . . 6 |- ( .r ` ndx ) e. NN
123	61	mpoexg 6437	. . . . . . 7 |- ( ( B e. _V /\ B e. _V ) -> .X. e. _V )
124	113, 113, 123	syl2anc 415	. . . . . 6 |- ( ph -> .X. e. _V )
125		opexg 4363	. . . . . 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 4585	. . . . 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 13484	. . . . . . 7 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
130	129	simpri 113	. . . . . 6 |- (Scalar ` ndx ) e. NN
131		opexg 4363	. . . . . 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 13494	. . . . . . 7 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
134	133	simpri 113	. . . . . 6 |- ( .s ` ndx ) e. NN
135	72	mpoexg 6437	. . . . . . 7 |- ( ( K e. _V /\ B e. _V ) -> .xb e. _V )
136	99, 113, 135	syl2anc 415	. . . . . 6 |- ( ph -> .xb e. _V )
137		opexg 4363	. . . . . 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 13520	. . . . . 6 |- (TopSet ` ndx ) e. NN
140		topnfn 13575	. . . . . . . . . . . 12 |- TopOpen Fn _V
141		funfvex 5707	. . . . . . . . . . . . 13 |- ( ( Fun TopOpen /\ R e. dom TopOpen ) -> ( TopOpen ` R ) e. _V )
142	141	funfni 5478	. . . . . . . . . . . 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 4316	. . . . . . . . . 10 |- ( O e. _V -> { O } e. _V )
146	144, 145	syl 14	. . . . . . . . 9 |- ( ph -> { O } e. _V )
147		xpexg 4884	. . . . . . . . 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 13595	. . . . . . . 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 4363	. . . . . 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 4585	. . . . 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 4584	. . . 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 6206	. 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 >. } ) )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   {cab 2224   {crab 2532   _Vcvv 2821   [_csb 3147   u. cun 3218   {csn 3705   {ctp 3707   <.cop 3708   class class class wbr 4125   |-> cmpt 4187   X. cxp 4767   `'ccnv 4768   |` cres 4771   "cima 4772   Fn wfn 5367   -->wf 5368   ` cfv 5372  (class class class)co 6075   e. cmpo 6077   oFcof 6290   oRcofr 6291   ^m cmap 6912   Fincfn 7012   <_ cle 8351   - cmin 8487   NNcn 9283   NN0cn0 9542   ndxcnx 13327  Slot cslot 13329   Basecbs 13330   +g cplusg 13408   .rcmulr 13409  Scalarcsca 13411   .scvsca 13412  TopSetcts 13414   TopOpenctopn 13571   Xt_cpt 13586   gsum_g cgsu 14127   mPwSer cmps 14968

This theorem was proved from 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 4241  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-cnex 8260  ax-resscn 8261  ax-1cn 8262  ax-1re 8263  ax-icn 8264  ax-addcl 8265  ax-addrcl 8266  ax-mulcl 8267  ax-i2m1 8274

This theorem 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 3687  df-sn 3711  df-pr 3712  df-tp 3713  df-op 3714  df-uni 3931  df-int 3966  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-ov 6078  df-oprab 6079  df-mpo 6080  df-of 6292  df-1st 6364  df-2nd 6365  df-map 6914  df-ixp 6971  df-inn 9284  df-2 9342  df-3 9343  df-4 9344  df-5 9345  df-6 9346  df-7 9347  df-8 9348  df-9 9349  df-n0 9543  df-ndx 13333  df-slot 13334  df-base 13336  df-plusg 13421  df-mulr 13422  df-sca 13424  df-vsca 13425  df-tset 13427  df-rest 13572  df-topn 13573  df-topgen 13591  df-pt 13592  df-psr 14970

This theorem is referenced by:  psrbasg  14988  psrplusgg  14992