Theorem psrval 13969

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 13967	. . . 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 5916	. . . . . . 7 |- ( ( ph /\ ( i = I /\ r = R ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
6	5	rabeqdv 2746	. . . . . 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 2240	. . . . 5 |- ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
9	8	csbeq1d 3079	. . . 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 9217	. . . . . . . . 9 |- NN0 e. _V
11		vex 2755	. . . . . . . . 9 |- i e. _V
12	10, 11	mapval 6690	. . . . . . . 8 |- ( NN0 ^m i ) = { f | f : i --> NN0 }
13		mapex 6684	. . . . . . . . 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 2262	. . . . . . 7 |- ( NN0 ^m i ) e. _V
16	15	rabex 4165	. . . . . 6 |- { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
17	8, 16	eqeltrrdi 2281	. . . . 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 5541	. . . . . . . . . 10 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = ( Base ` R ) )
20		psrval.k	. . . . . . . . . 10 |- K = ( Base ` R )
21	19, 20	eqtr4di 2240	. . . . . . . . 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 5918	. . . . . . . 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 2225	. . . . . . 7 |- ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = B )
27	26	csbeq1d 3079	. . . . . 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 12581	. . . . . . . . . . 11 |- Base Fn _V
29		vex 2755	. . . . . . . . . . 11 |- r e. _V
30		funfvex 5554	. . . . . . . . . . . 12 |- ( ( Fun Base /\ r e. dom Base ) -> ( Base ` r ) e. _V )
31	30	funfni 5338	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ r e. _V ) -> ( Base ` r ) e. _V )
32	28, 29, 31	mp2an 426	. . . . . . . . . 10 |- ( Base ` r ) e. _V
33		vex 2755	. . . . . . . . . 10 |- d e. _V
34	32, 33	mapval 6690	. . . . . . . . 9 |- ( ( Base ` r ) ^m d ) = { f | f : d --> ( Base ` r ) }
35		mapex 6684	. . . . . . . . . 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 2262	. . . . . . . 8 |- ( ( Base ` r ) ^m d ) e. _V
38	26, 37	eqeltrrdi 2281	. . . . . . 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 3803	. . . . . . . . 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 5541	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
43		psrval.a	. . . . . . . . . . . . . 14 |- .+ = ( +g ` R )
44	42, 43	eqtr4di 2240	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = .+ )
45	44	ofeqd 6112	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
46	39, 39	xpeq12d 4672	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
47	45, 46	reseq12d 4929	. . . . . . . . . . 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 2240	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = .+b )
50	49	opeq2d 3803	. . . . . . . . 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 2746	. . . . . . . . . . . . . . 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 5541	. . . . . . . . . . . . . . . . 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 2240	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = .x. )
56	55	oveqd 5917	. . . . . . . . . . . . . . 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 4103	. . . . . . . . . . . . . 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 5918	. . . . . . . . . . . . 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 4103	. . . . . . . . . . . 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 5962	. . . . . . . . . . 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 2240	. . . . . . . . . 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 3803	. . . . . . . . 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 3702	. . . . . . . 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 3803	. . . . . . . . 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 6112	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
68	51	xpeq1d 4670	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { x } ) = ( D X. { x } ) )
69		eqidd 2190	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> f = f )
70	67, 68, 69	oveq123d 5921	. . . . . . . . . . . 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 5962	. . . . . . . . . . 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 2240	. . . . . . . . . 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 3803	. . . . . . . . 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 5541	. . . . . . . . . . . . . . 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 2240	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = O )
78	77	sneqd 3623	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
79	51, 78	xpeq12d 4672	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
80	79	fveq2d 5541	. . . . . . . . . . 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 2225	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = J )
84	83	opeq2d 3803	. . . . . . . . 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 3702	. . . . . . . 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 3305	. . . . . . 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 3118	. . . . . 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 2222	. . . . 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 3118	. . . 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 2222	. . 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 2765	. . 3 |- ( ph -> I e. _V )
93		psrval.r	. . . 4 |- ( ph -> R e. X )
94	93	elexd 2765	. . 3 |- ( ph -> R e. _V )
95		basendxnn 12579	. . . . . 6 |- ( Base ` ndx ) e. NN
96		funfvex 5554	. . . . . . . . . . . 12 |- ( ( Fun Base /\ R e. dom Base ) -> ( Base ` R ) e. _V )
97	96	funfni 5338	. . . . . . . . . . 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 2276	. . . . . . . . 9 |- ( ph -> K e. _V )
100		mapvalg 6688	. . . . . . . . . . . . 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 6684	. . . . . . . . . . . . 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 2266	. . . . . . . . . . 11 |- ( ph -> ( NN0 ^m I ) e. _V )
105		rabexg 4164	. . . . . . . . . . 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 2276	. . . . . . . . 9 |- ( ph -> D e. _V )
108		mapvalg 6688	. . . . . . . . 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 6684	. . . . . . . . 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 2266	. . . . . . 7 |- ( ph -> ( K ^m D ) e. _V )
113	24, 112	eqeltrd 2266	. . . . . 6 |- ( ph -> B e. _V )
114		opexg 4249	. . . . . 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 12634	. . . . . 6 |- ( +g ` ndx ) e. NN
117	113, 113	ofmresex 6166	. . . . . . 7 |- ( ph -> ( oF .+ |` ( B X. B ) ) e. _V )
118	48, 117	eqeltrid 2276	. . . . . 6 |- ( ph -> .+b e. _V )
119		opexg 4249	. . . . . 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 12654	. . . . . . 7 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
122	121	simpri 113	. . . . . 6 |- ( .r ` ndx ) e. NN
123	61	mpoexg 6240	. . . . . . 7 |- ( ( B e. _V /\ B e. _V ) -> .X. e. _V )
124	113, 113, 123	syl2anc 411	. . . . . 6 |- ( ph -> .X. e. _V )
125		opexg 4249	. . . . . 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 4465	. . . . 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 12675	. . . . . . 7 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
130	129	simpri 113	. . . . . 6 |- (Scalar ` ndx ) e. NN
131		opexg 4249	. . . . . 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 12685	. . . . . . 7 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
134	133	simpri 113	. . . . . 6 |- ( .s ` ndx ) e. NN
135	72	mpoexg 6240	. . . . . . 7 |- ( ( K e. _V /\ B e. _V ) -> .xb e. _V )
136	99, 113, 135	syl2anc 411	. . . . . 6 |- ( ph -> .xb e. _V )
137		opexg 4249	. . . . . 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 12711	. . . . . 6 |- (TopSet ` ndx ) e. NN
140		topnfn 12760	. . . . . . . . . . . 12 |- TopOpen Fn _V
141		funfvex 5554	. . . . . . . . . . . . 13 |- ( ( Fun TopOpen /\ R e. dom TopOpen ) -> ( TopOpen ` R ) e. _V )
142	141	funfni 5338	. . . . . . . . . . . 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 2276	. . . . . . . . . 10 |- ( ph -> O e. _V )
145		snexg 4205	. . . . . . . . . 10 |- ( O e. _V -> { O } e. _V )
146	144, 145	syl 14	. . . . . . . . 9 |- ( ph -> { O } e. _V )
147		xpexg 4761	. . . . . . . . 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 12780	. . . . . . . 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 2266	. . . . . 6 |- ( ph -> J e. _V )
152		opexg 4249	. . . . . 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 4465	. . . . 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 4464	. . . 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 6028	. 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 2234	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 2160   {cab 2175   {crab 2472   _Vcvv 2752   [_csb 3072   u. cun 3142   {csn 3610   {ctp 3612   <.cop 3613   class class class wbr 4021   |-> cmpt 4082   X. cxp 4645   `'ccnv 4646   |` cres 4649   "cima 4650   Fn wfn 5233   -->wf 5234   ` cfv 5238  (class class class)co 5900   e. cmpo 5902   oFcof 6108   oRcofr 6109   ^m cmap 6678   Fincfn 6770   <_ cle 8028   - cmin 8163   NNcn 8954   NN0cn0 9211   ndxcnx 12520  Slot cslot 12522   Basecbs 12523   +g cplusg 12600   .rcmulr 12601  Scalarcsca 12603   .scvsca 12604  TopSetcts 12606   TopOpenctopn 12756   Xt_cpt 12771   gsum_g cgsu 12773   mPwSer cmps 13966

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4136  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-un 4454  ax-setind 4557  ax-cnex 7937  ax-resscn 7938  ax-1cn 7939  ax-1re 7940  ax-icn 7941  ax-addcl 7942  ax-addrcl 7943  ax-mulcl 7944  ax-i2m1 7951

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-tp 3618  df-op 3619  df-uni 3828  df-int 3863  df-iun 3906  df-br 4022  df-opab 4083  df-mpt 4084  df-id 4314  df-xp 4653  df-rel 4654  df-cnv 4655  df-co 4656  df-dm 4657  df-rn 4658  df-res 4659  df-ima 4660  df-iota 5199  df-fun 5240  df-fn 5241  df-f 5242  df-f1 5243  df-fo 5244  df-f1o 5245  df-fv 5246  df-ov 5903  df-oprab 5904  df-mpo 5905  df-of 6110  df-1st 6169  df-2nd 6170  df-map 6680  df-ixp 6729  df-inn 8955  df-2 9013  df-3 9014  df-4 9015  df-5 9016  df-6 9017  df-7 9018  df-8 9019  df-9 9020  df-n0 9212  df-ndx 12526  df-slot 12527  df-base 12529  df-plusg 12613  df-mulr 12614  df-sca 12616  df-vsca 12617  df-tset 12619  df-rest 12757  df-topn 12758  df-topgen 12776  df-pt 12777  df-psr 13967

This theorem is referenced by:  psrbasg  13976  psrplusgg  13979