Theorem psrval 14624

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 14621	. . . 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 529	. . . . . . . 8 |- ( ( ph /\ ( i = I /\ r = R ) ) -> i = I )
5	4	oveq2d 6016	. . . . . . 7 |- ( ( ph /\ ( i = I /\ r = R ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
6	5	rabeqdv 2793	. . . . . 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 2280	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
9	8	csbeq1d 3131	. . . 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 9371	. . . . . . . . 9 |- NN0 e. _V
11		vex 2802	. . . . . . . . 9 |- i e. _V
12	10, 11	mapval 6805	. . . . . . . 8 |- ( NN0 ^m i ) = { f | f : i --> NN0 }
13		mapex 6799	. . . . . . . . 9 |- ( ( i e. _V /\ NN0 e. _V ) -> { f | f : i --> NN0 } e. _V )
14	11, 10, 13	mp2an 426	. . . . . . . 8 |- { f | f : i --> NN0 } e. _V
15	12, 14	eqeltri 2302	. . . . . . 7 |- ( NN0 ^m i ) e. _V
16	15	rabex 4227	. . . . . 6 |- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
17	8, 16	eqeltrrdi 2321	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> D e. _V )
18		simplrr 536	. . . . . . . . . . 11 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> r = R )
19	18	fveq2d 5630	. . . . . . . . . 10 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = ( Base ` R ) )
20		psrval.k	. . . . . . . . . 10 |- K = ( Base ` R )
21	19, 20	eqtr4di 2280	. . . . . . . . 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 6018	. . . . . . . 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 488	. . . . . . . 8 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B = ( K ^m D ) )
26	23, 25	eqtr4d 2265	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = B )
27	26	csbeq1d 3131	. . . . . 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 13086	. . . . . . . . . . 11 |- Base Fn _V
29		vex 2802	. . . . . . . . . . 11 |- r e. _V
30		funfvex 5643	. . . . . . . . . . . 12 |- ( ( Fun Base /\ r e. dom Base ) -> ( Base ` r ) e. _V )
31	30	funfni 5422	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ r e. _V ) -> ( Base ` r ) e. _V )
32	28, 29, 31	mp2an 426	. . . . . . . . . 10 |- ( Base ` r ) e. _V
33		vex 2802	. . . . . . . . . 10 |- d e. _V
34	32, 33	mapval 6805	. . . . . . . . 9 |- ( ( Base ` r ) ^m d ) = { f | f : d --> ( Base ` r ) }
35		mapex 6799	. . . . . . . . . 10 |- ( ( d e. _V /\ ( Base ` r ) e. _V ) -> { f | f : d --> ( Base ` r ) } e. _V )
36	33, 32, 35	mp2an 426	. . . . . . . . 9 |- { f | f : d --> ( Base ` r ) } e. _V
37	34, 36	eqeltri 2302	. . . . . . . 8 |- ( ( Base ` r ) ^m d ) e. _V
38	26, 37	eqeltrrdi 2321	. . . . . . 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 3863	. . . . . . . . 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 5630	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
43		psrval.a	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
44	42, 43	eqtr4di 2280	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = .+ )
45	44	ofeqd 6218	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
46	39, 39	xpeq12d 4743	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
47	45, 46	reseq12d 5005	. . . . . . . . . . 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 2280	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = .+b )
50	49	opeq2d 3863	. . . . . . . . 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 2793	. . . . . . . . . . . . . . 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 5630	. . . . . . . . . . . . . . . . 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 2280	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = .x. )
56	55	oveqd 6017	. . . . . . . . . . . . . . 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 4165	. . . . . . . . . . . . . 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 6018	. . . . . . . . . . . . 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 4165	. . . . . . . . . . . 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 6065	. . . . . . . . . . 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 2280	. . . . . . . . . 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 3863	. . . . . . . . 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 3758	. . . . . . . 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 3863	. . . . . . . . 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 6218	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
68	51	xpeq1d 4741	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { x } ) = ( D X. { x } ) )
69		eqidd 2230	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> f = f )
70	67, 68, 69	oveq123d 6021	. . . . . . . . . . . 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 6065	. . . . . . . . . . 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 2280	. . . . . . . . . 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 3863	. . . . . . . . 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 5630	. . . . . . . . . . . . . . 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 2280	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = O )
78	77	sneqd 3679	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
79	51, 78	xpeq12d 4743	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
80	79	fveq2d 5630	. . . . . . . . . . 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 492	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> J = ( Xt_ ` ( D X. { O } ) ) )
83	80, 82	eqtr4d 2265	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = J )
84	83	opeq2d 3863	. . . . . . . . 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 3758	. . . . . . . 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 3359	. . . . . . 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 3171	. . . . . 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 2262	. . . . 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 3171	. . . 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 2262	. . 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 2813	. . 3 |- ( ph -> I e. _V )
93		psrval.r	. . . 4 |- ( ph -> R e. X )
94	93	elexd 2813	. . 3 |- ( ph -> R e. _V )
95		basendxnn 13083	. . . . . 6 |- ( Base ` ndx ) e. NN
96		funfvex 5643	. . . . . . . . . . . 12 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
97	96	funfni 5422	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ R e. _V ) -> ( Base ` R ) e. _V )
98	28, 94, 97	sylancr 414	. . . . . . . . . 10 |- ( ph -> ( Base ` R ) e. _V )
99	20, 98	eqeltrid 2316	. . . . . . . . 9 |- ( ph -> K e. _V )
100		mapvalg 6803	. . . . . . . . . . . . 13 |- ( ( NN0 e. _V /\ I e. W ) -> ( NN0 ^m I ) = { f | f : I --> NN0 } )
101	10, 91, 100	sylancr 414	. . . . . . . . . . . 12 |- ( ph -> ( NN0 ^m I ) = { f | f : I --> NN0 } )
102		mapex 6799	. . . . . . . . . . . . 13 |- ( ( I e. W /\ NN0 e. _V ) -> { f | f : I --> NN0 } e. _V )
103	91, 10, 102	sylancl 413	. . . . . . . . . . . 12 |- ( ph -> { f | f : I --> NN0 } e. _V )
104	101, 103	eqeltrd 2306	. . . . . . . . . . 11 |- ( ph -> ( NN0 ^m I ) e. _V )
105		rabexg 4226	. . . . . . . . . . 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 2316	. . . . . . . . 9 |- ( ph -> D e. _V )
108		mapvalg 6803	. . . . . . . . 9 |- ( ( K e. _V /\ D e. _V ) -> ( K ^m D ) = { f | f : D --> K } )
109	99, 107, 108	syl2anc 411	. . . . . . . 8 |- ( ph -> ( K ^m D ) = { f | f : D --> K } )
110		mapex 6799	. . . . . . . . 9 |- ( ( D e. _V /\ K e. _V ) -> { f | f : D --> K } e. _V )
111	107, 99, 110	syl2anc 411	. . . . . . . 8 |- ( ph -> { f | f : D --> K } e. _V )
112	109, 111	eqeltrd 2306	. . . . . . 7 |- ( ph -> ( K ^m D ) e. _V )
113	24, 112	eqeltrd 2306	. . . . . 6 |- ( ph -> B e. _V )
114		opexg 4313	. . . . . 6 |- ( ( ( Base ` ndx ) e. NN /\ B e. _V ) -> <. ( Base ` ndx ) , B >. e. _V )
115	95, 113, 114	sylancr 414	. . . . 5 |- ( ph -> <. ( Base ` ndx ) , B >. e. _V )
116		plusgndxnn 13139	. . . . . 6 |- ( +g ` ndx ) e. NN
117	113, 113	ofmresex 6280	. . . . . . 7 |- ( ph -> ( oF .+ |` ( B X. B ) ) e. _V )
118	48, 117	eqeltrid 2316	. . . . . 6 |- ( ph -> .+b e. _V )
119		opexg 4313	. . . . . 6 |- ( ( ( +g ` ndx ) e. NN /\ .+b e. _V ) -> <. ( +g ` ndx ) , .+b >. e. _V )
120	116, 118, 119	sylancr 414	. . . . 5 |- ( ph -> <. ( +g ` ndx ) , .+b >. e. _V )
121		mulrslid 13160	. . . . . . 7 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
122	121	simpri 113	. . . . . 6 |- ( .r ` ndx ) e. NN
123	61	mpoexg 6355	. . . . . . 7 |- ( ( B e. _V /\ B e. _V ) -> .X. e. _V )
124	113, 113, 123	syl2anc 411	. . . . . 6 |- ( ph -> .X. e. _V )
125		opexg 4313	. . . . . 6 |- ( ( ( .r ` ndx ) e. NN /\ .X. e. _V ) -> <. ( .r ` ndx ) , .X. >. e. _V )
126	122, 124, 125	sylancr 414	. . . . 5 |- ( ph -> <. ( .r ` ndx ) , .X. >. e. _V )
127		tpexg 4534	. . . . 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 1271	. . . 4 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V )
129		scaslid 13181	. . . . . . 7 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
130	129	simpri 113	. . . . . 6 |- (Scalar ` ndx ) e. NN
131		opexg 4313	. . . . . 6 |- ( ( (Scalar ` ndx ) e. NN /\ R e. X ) -> <. (Scalar ` ndx ) , R >. e. _V )
132	130, 93, 131	sylancr 414	. . . . 5 |- ( ph -> <. (Scalar ` ndx ) , R >. e. _V )
133		vscaslid 13191	. . . . . . 7 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
134	133	simpri 113	. . . . . 6 |- ( .s ` ndx ) e. NN
135	72	mpoexg 6355	. . . . . . 7 |- ( ( K e. _V /\ B e. _V ) -> .xb e. _V )
136	99, 113, 135	syl2anc 411	. . . . . 6 |- ( ph -> .xb e. _V )
137		opexg 4313	. . . . . 6 |- ( ( ( .s ` ndx ) e. NN /\ .xb e. _V ) -> <. ( .s ` ndx ) , .xb >. e. _V )
138	134, 136, 137	sylancr 414	. . . . 5 |- ( ph -> <. ( .s ` ndx ) , .xb >. e. _V )
139		tsetndxnn 13217	. . . . . 6 |- (TopSet ` ndx ) e. NN
140		topnfn 13272	. . . . . . . . . . . 12 |- TopOpen Fn _V
141		funfvex 5643	. . . . . . . . . . . . 13 |- ( ( Fun TopOpen /\ R e. dom TopOpen ) -> ( TopOpen ` R ) e. _V )
142	141	funfni 5422	. . . . . . . . . . . 12 |- ( ( TopOpen Fn _V /\ R e. _V ) -> ( TopOpen ` R ) e. _V )
143	140, 94, 142	sylancr 414	. . . . . . . . . . 11 |- ( ph -> ( TopOpen ` R ) e. _V )
144	76, 143	eqeltrid 2316	. . . . . . . . . 10 |- ( ph -> O e. _V )
145		snexg 4267	. . . . . . . . . 10 |- ( O e. _V -> { O } e. _V )
146	144, 145	syl 14	. . . . . . . . 9 |- ( ph -> { O } e. _V )
147		xpexg 4832	. . . . . . . . 9 |- ( ( D e. _V /\ { O } e. _V ) -> ( D X. { O } ) e. _V )
148	107, 146, 147	syl2anc 411	. . . . . . . 8 |- ( ph -> ( D X. { O } ) e. _V )
149		ptex 13292	. . . . . . . 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 2306	. . . . . 6 |- ( ph -> J e. _V )
152		opexg 4313	. . . . . 6 |- ( ( (TopSet ` ndx ) e. NN /\ J e. _V ) -> <. (TopSet ` ndx ) , J >. e. _V )
153	139, 151, 152	sylancr 414	. . . . 5 |- ( ph -> <. (TopSet ` ndx ) , J >. e. _V )
154		tpexg 4534	. . . . 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 1271	. . . 4 |- ( ph -> { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } e. _V )
156		unexg 4533	. . . 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 411	. . 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 6131	. 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 2274	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 1395   e. wcel 2200   {cab 2215   {crab 2512   _Vcvv 2799   [_csb 3124   u. cun 3195   {csn 3666   {ctp 3668   <.cop 3669   class class class wbr 4082   |-> cmpt 4144   X. cxp 4716   `'ccnv 4717   |` cres 4720   "cima 4721   Fn wfn 5312   -->wf 5313   ` cfv 5317  (class class class)co 6000   e. cmpo 6002   oFcof 6214   oRcofr 6215   ^m cmap 6793   Fincfn 6885   <_ cle 8178   - cmin 8313   NNcn 9106   NN0cn0 9365   ndxcnx 13024  Slot cslot 13026   Basecbs 13027   +g cplusg 13105   .rcmulr 13106  Scalarcsca 13108   .scvsca 13109  TopSetcts 13111   TopOpenctopn 13268   Xt_cpt 13283   gsum_g cgsu 13285   mPwSer cmps 14619

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4198  ax-sep 4201  ax-pow 4257  ax-pr 4292  ax-un 4523  ax-setind 4628  ax-cnex 8086  ax-resscn 8087  ax-1cn 8088  ax-1re 8089  ax-icn 8090  ax-addcl 8091  ax-addrcl 8092  ax-mulcl 8093  ax-i2m1 8100

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-tp 3674  df-op 3675  df-uni 3888  df-int 3923  df-iun 3966  df-br 4083  df-opab 4145  df-mpt 4146  df-id 4383  df-xp 4724  df-rel 4725  df-cnv 4726  df-co 4727  df-dm 4728  df-rn 4729  df-res 4730  df-ima 4731  df-iota 5277  df-fun 5319  df-fn 5320  df-f 5321  df-f1 5322  df-fo 5323  df-f1o 5324  df-fv 5325  df-ov 6003  df-oprab 6004  df-mpo 6005  df-of 6216  df-1st 6284  df-2nd 6285  df-map 6795  df-ixp 6844  df-inn 9107  df-2 9165  df-3 9166  df-4 9167  df-5 9168  df-6 9169  df-7 9170  df-8 9171  df-9 9172  df-n0 9366  df-ndx 13030  df-slot 13031  df-base 13033  df-plusg 13118  df-mulr 13119  df-sca 13121  df-vsca 13122  df-tset 13124  df-rest 13269  df-topn 13270  df-topgen 13288  df-pt 13289  df-psr 14621

This theorem is referenced by:  psrbasg  14632  psrplusgg  14636