Metamath Proof Explorer

Theorem psrval

Description: Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses 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 gsum ( 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 psrval 
|- ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. ( TopSet ` ndx ) , J >. } ) )

Proof

Step Hyp Ref Expression
1 psrval.s 
 |-  S = ( I mPwSer R )
2 psrval.k 
 |-  K = ( Base ` R )
3 psrval.a 
 |-  .+ = ( +g ` R )
4 psrval.m 
 |-  .x. = ( .r ` R )
5 psrval.o 
 |-  O = ( TopOpen ` R )
6 psrval.d 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
7 psrval.b 
 |-  ( ph -> B = ( K ^m D ) )
8 psrval.p 
 |-  .+b = ( oF .+ |` ( B X. B ) )
9 psrval.t 
 |-  .X. = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
10 psrval.v 
 |-  .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )
11 psrval.j 
 |-  ( ph -> J = ( Xt_ ` ( D X. { O } ) ) )
12 psrval.i 
 |-  ( ph -> I e. W )
13 psrval.r 
 |-  ( ph -> R e. X )
14 df-psr 
 |-  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 gsum ( 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 ) } ) ) >. } ) )
15 14 a1i 
 |-  ( 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 gsum ( 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 ) } ) ) >. } ) ) )
16 simprl 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> i = I )
17 16 oveq2d 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> ( NN0 ^m i ) = ( NN0 ^m I ) )
18 rabeq 
 |-  ( ( NN0 ^m i ) = ( NN0 ^m I ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
19 17 18 syl 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
20 19 6 eqtr4di 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } = D )
21 20 csbeq1d 
 |-  ( ( 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 gsum ( 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 gsum ( 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 ) } ) ) >. } ) )
22 ovex 
 |-  ( NN0 ^m i ) e. _V
23 22 rabex 
 |-  { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } e. _V
24 20 23 eqeltrrdi 
 |-  ( ( ph /\ ( i = I /\ r = R ) ) -> D e. _V )
25 simplrr 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> r = R )
26 25 fveq2d 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = ( Base ` R ) )
27 26 2 eqtr4di 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( Base ` r ) = K )
28 simpr 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> d = D )
29 27 28 oveq12d 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = ( K ^m D ) )
30 7 ad2antrr 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B = ( K ^m D ) )
31 29 30 eqtr4d 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> ( ( Base ` r ) ^m d ) = B )
32 31 csbeq1d 
 |-  ( ( ( 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 gsum ( 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 gsum ( 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 ) } ) ) >. } ) )
33 ovex 
 |-  ( ( Base ` r ) ^m d ) e. _V
34 31 33 eqeltrrdi 
 |-  ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) -> B e. _V )
35 simpr 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> b = B )
36 35 opeq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
37 25 adantr 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> r = R )
38 37 fveq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = ( +g ` R ) )
39 38 3 eqtr4di 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( +g ` r ) = .+ )
40 39 ofeqd 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( +g ` r ) = oF .+ )
41 35 35 xpeq12d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
42 40 41 reseq12d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = ( oF .+ |` ( B X. B ) ) )
43 42 8 eqtr4di 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( oF ( +g ` r ) |` ( b X. b ) ) = .+b )
44 43 opeq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. = <. ( +g ` ndx ) , .+b >. )
45 28 adantr 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> d = D )
46 rabeq 
 |-  ( d = D -> { y e. d | y oR <_ k } = { y e. D | y oR <_ k } )
47 45 46 syl 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { y e. d | y oR <_ k } = { y e. D | y oR <_ k } )
48 37 fveq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = ( .r ` R ) )
49 48 4 eqtr4di 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( .r ` r ) = .x. )
50 49 oveqd 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) = ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) )
51 47 50 mpteq12dv 
 |-  ( ( ( ( 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 ) ) ) ) )
52 37 51 oveq12d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) = ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) )
53 45 52 mpteq12dv 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) = ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )
54 35 35 53 mpoeq123dv 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( 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 gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) )
55 54 9 eqtr4di 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) = .X. )
56 55 opeq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsum ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. = <. ( .r ` ndx ) , .X. >. )
57 36 44 56 tpeq123d 
 |-  ( ( ( ( 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 gsum ( 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. >. } )
58 37 opeq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( Scalar ` ndx ) , r >. = <. ( Scalar ` ndx ) , R >. )
59 27 adantr 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Base ` r ) = K )
60 49 ofeqd 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> oF ( .r ` r ) = oF .x. )
61 45 xpeq1d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { x } ) = ( D X. { x } ) )
62 eqidd 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> f = f )
63 60 61 62 oveq123d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( ( d X. { x } ) oF ( .r ` r ) f ) = ( ( D X. { x } ) oF .x. f ) )
64 59 35 63 mpoeq123dv 
 |-  ( ( ( ( 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 ) ) )
65 64 10 eqtr4di 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) = .xb )
66 65 opeq2d 
 |-  ( ( ( ( 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 >. )
67 37 fveq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = ( TopOpen ` R ) )
68 67 5 eqtr4di 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( TopOpen ` r ) = O )
69 68 sneqd 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> { ( TopOpen ` r ) } = { O } )
70 45 69 xpeq12d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( d X. { ( TopOpen ` r ) } ) = ( D X. { O } ) )
71 70 fveq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = ( Xt_ ` ( D X. { O } ) ) )
72 11 ad3antrrr 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> J = ( Xt_ ` ( D X. { O } ) ) )
73 71 72 eqtr4d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) = J )
74 73 opeq2d 
 |-  ( ( ( ( ph /\ ( i = I /\ r = R ) ) /\ d = D ) /\ b = B ) -> <. ( TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. = <. ( TopSet ` ndx ) , J >. )
75 58 66 74 tpeq123d 
 |-  ( ( ( ( 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 >. } )
76 57 75 uneq12d 
 |-  ( ( ( ( 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 gsum ( 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 >. } ) )
77 34 76 csbied 
 |-  ( ( ( 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 gsum ( 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 >. } ) )
78 32 77 eqtrd 
 |-  ( ( ( 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 gsum ( 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 >. } ) )
79 24 78 csbied 
 |-  ( ( 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 gsum ( 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 >. } ) )
80 21 79 eqtrd 
 |-  ( ( 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 gsum ( 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 >. } ) )
81 12 elexd 
 |-  ( ph -> I e. _V )
82 13 elexd 
 |-  ( ph -> R e. _V )
83 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } e. _V
84 tpex 
 |-  { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. ( TopSet ` ndx ) , J >. } e. _V
85 83 84 unex 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. ( TopSet ` ndx ) , J >. } ) e. _V
86 85 a1i 
 |-  ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. ( TopSet ` ndx ) , J >. } ) e. _V )
87 15 80 81 82 86 ovmpod 
 |-  ( ph -> ( I mPwSer R ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. ( TopSet ` ndx ) , J >. } ) )
88 1 87 eqtrid 
 |-  ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. ( TopSet ` ndx ) , J >. } ) )