Theorem psrval 14220

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 14218	. . . 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 5938	. . . . . . 7 |- ( ( ph /\ ( i = I /\ r = R ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
6	5	rabeqdv 2757	. . . . . 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 2247	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
9	8	csbeq1d 3091	. . . 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 9255	. . . . . . . . 9 |- NN0 e. _V
11		vex 2766	. . . . . . . . 9 |- i e. _V
12	10, 11	mapval 6719	. . . . . . . 8 |- ( NN0 ^m i ) = { f | f : i --> NN0 }
13		mapex 6713	. . . . . . . . 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 2269	. . . . . . 7 |- ( NN0 ^m i ) e. _V
16	15	rabex 4177	. . . . . 6 |- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
17	8, 16	eqeltrrdi 2288	. . . . 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 5562	. . . . . . . . . 10 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = ( Base ` R ) )
20		psrval.k	. . . . . . . . . 10 |- K = ( Base ` R )
21	19, 20	eqtr4di 2247	. . . . . . . . 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 5940	. . . . . . . 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 2232	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = B )
27	26	csbeq1d 3091	. . . . . 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 12736	. . . . . . . . . . 11 |- Base Fn _V
29		vex 2766	. . . . . . . . . . 11 |- r e. _V
30		funfvex 5575	. . . . . . . . . . . 12 |- ( ( Fun Base /\ r e. dom Base ) -> ( Base ` r ) e. _V )
31	30	funfni 5358	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ r e. _V ) -> ( Base ` r ) e. _V )
32	28, 29, 31	mp2an 426	. . . . . . . . . 10 |- ( Base ` r ) e. _V
33		vex 2766	. . . . . . . . . 10 |- d e. _V
34	32, 33	mapval 6719	. . . . . . . . 9 |- ( ( Base ` r ) ^m d ) = { f | f : d --> ( Base ` r ) }
35		mapex 6713	. . . . . . . . . 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 2269	. . . . . . . 8 |- ( ( Base ` r ) ^m d ) e. _V
38	26, 37	eqeltrrdi 2288	. . . . . . 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 3815	. . . . . . . . 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 5562	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
43		psrval.a	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
44	42, 43	eqtr4di 2247	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = .+ )
45	44	ofeqd 6137	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
46	39, 39	xpeq12d 4688	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
47	45, 46	reseq12d 4947	. . . . . . . . . . 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 2247	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = .+b )
50	49	opeq2d 3815	. . . . . . . . 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 2757	. . . . . . . . . . . . . . 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 5562	. . . . . . . . . . . . . . . . 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 2247	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = .x. )
56	55	oveqd 5939	. . . . . . . . . . . . . . 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 4115	. . . . . . . . . . . . . 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 5940	. . . . . . . . . . . . 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 4115	. . . . . . . . . . . 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 5984	. . . . . . . . . . 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 2247	. . . . . . . . . 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 3815	. . . . . . . . 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 3714	. . . . . . . 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 3815	. . . . . . . . 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 6137	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
68	51	xpeq1d 4686	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { x } ) = ( D X. { x } ) )
69		eqidd 2197	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> f = f )
70	67, 68, 69	oveq123d 5943	. . . . . . . . . . . 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 5984	. . . . . . . . . . 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 2247	. . . . . . . . . 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 3815	. . . . . . . . 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 5562	. . . . . . . . . . . . . . 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 2247	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = O )
78	77	sneqd 3635	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
79	51, 78	xpeq12d 4688	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
80	79	fveq2d 5562	. . . . . . . . . . 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 2232	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = J )
84	83	opeq2d 3815	. . . . . . . . 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 3714	. . . . . . . 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 3318	. . . . . . 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 3131	. . . . . 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 2229	. . . . 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 3131	. . . 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 2229	. . 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 2776	. . 3 |- ( ph -> I e. _V )
93		psrval.r	. . . 4 |- ( ph -> R e. X )
94	93	elexd 2776	. . 3 |- ( ph -> R e. _V )
95		basendxnn 12734	. . . . . 6 |- ( Base ` ndx ) e. NN
96		funfvex 5575	. . . . . . . . . . . 12 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
97	96	funfni 5358	. . . . . . . . . . 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 2283	. . . . . . . . 9 |- ( ph -> K e. _V )
100		mapvalg 6717	. . . . . . . . . . . . 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 6713	. . . . . . . . . . . . 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 2273	. . . . . . . . . . 11 |- ( ph -> ( NN0 ^m I ) e. _V )
105		rabexg 4176	. . . . . . . . . . 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 2283	. . . . . . . . 9 |- ( ph -> D e. _V )
108		mapvalg 6717	. . . . . . . . 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 6713	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> ( K ^m D ) e. _V )
113	24, 112	eqeltrd 2273	. . . . . 6 |- ( ph -> B e. _V )
114		opexg 4261	. . . . . 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 12789	. . . . . 6 |- ( +g ` ndx ) e. NN
117	113, 113	ofmresex 6194	. . . . . . 7 |- ( ph -> ( oF .+ |` ( B X. B ) ) e. _V )
118	48, 117	eqeltrid 2283	. . . . . 6 |- ( ph -> .+b e. _V )
119		opexg 4261	. . . . . 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 12809	. . . . . . 7 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
122	121	simpri 113	. . . . . 6 |- ( .r ` ndx ) e. NN
123	61	mpoexg 6269	. . . . . . 7 |- ( ( B e. _V /\ B e. _V ) -> .X. e. _V )
124	113, 113, 123	syl2anc 411	. . . . . 6 |- ( ph -> .X. e. _V )
125		opexg 4261	. . . . . 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 4479	. . . . 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 1249	. . . 4 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V )
129		scaslid 12830	. . . . . . 7 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
130	129	simpri 113	. . . . . 6 |- (Scalar ` ndx ) e. NN
131		opexg 4261	. . . . . 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 12840	. . . . . . 7 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
134	133	simpri 113	. . . . . 6 |- ( .s ` ndx ) e. NN
135	72	mpoexg 6269	. . . . . . 7 |- ( ( K e. _V /\ B e. _V ) -> .xb e. _V )
136	99, 113, 135	syl2anc 411	. . . . . 6 |- ( ph -> .xb e. _V )
137		opexg 4261	. . . . . 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 12866	. . . . . 6 |- (TopSet ` ndx ) e. NN
140		topnfn 12915	. . . . . . . . . . . 12 |- TopOpen Fn _V
141		funfvex 5575	. . . . . . . . . . . . 13 |- ( ( Fun TopOpen /\ R e. dom TopOpen ) -> ( TopOpen ` R ) e. _V )
142	141	funfni 5358	. . . . . . . . . . . 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 2283	. . . . . . . . . 10 |- ( ph -> O e. _V )
145		snexg 4217	. . . . . . . . . 10 |- ( O e. _V -> { O } e. _V )
146	144, 145	syl 14	. . . . . . . . 9 |- ( ph -> { O } e. _V )
147		xpexg 4777	. . . . . . . . 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 12935	. . . . . . . 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 2273	. . . . . 6 |- ( ph -> J e. _V )
152		opexg 4261	. . . . . 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 4479	. . . . 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 1249	. . . 4 |- ( ph -> { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } e. _V )
156		unexg 4478	. . . 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 6050	. 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 2241	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 1364   e. wcel 2167   {cab 2182   {crab 2479   _Vcvv 2763   [_csb 3084   u. cun 3155   {csn 3622   {ctp 3624   <.cop 3625   class class class wbr 4033   |-> cmpt 4094   X. cxp 4661   `'ccnv 4662   |` cres 4665   "cima 4666   Fn wfn 5253   -->wf 5254   ` cfv 5258  (class class class)co 5922   e. cmpo 5924   oFcof 6133   oRcofr 6134   ^m cmap 6707   Fincfn 6799   <_ cle 8062   - cmin 8197   NNcn 8990   NN0cn0 9249   ndxcnx 12675  Slot cslot 12677   Basecbs 12678   +g cplusg 12755   .rcmulr 12756  Scalarcsca 12758   .scvsca 12759  TopSetcts 12761   TopOpenctopn 12911   Xt_cpt 12926   gsum_g cgsu 12928   mPwSer cmps 14217

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-i2m1 7984

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-tp 3630  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-ov 5925  df-oprab 5926  df-mpo 5927  df-of 6135  df-1st 6198  df-2nd 6199  df-map 6709  df-ixp 6758  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-5 9052  df-6 9053  df-7 9054  df-8 9055  df-9 9056  df-n0 9250  df-ndx 12681  df-slot 12682  df-base 12684  df-plusg 12768  df-mulr 12769  df-sca 12771  df-vsca 12772  df-tset 12774  df-rest 12912  df-topn 12913  df-topgen 12931  df-pt 12932  df-psr 14218

This theorem is referenced by:  psrbasg  14227  psrplusgg  14230