Metamath Proof Explorer

Theorem imasval

Description: Value of an image structure. (Contributed by Mario Carneiro, 23-Feb-2015) (Revised by Mario Carneiro, 11-Jul-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 6-Oct-2020)

Ref Expression
Hypotheses imasval.u 
|- ( ph -> U = ( F "s R ) )
imasval.v 
|- ( ph -> V = ( Base ` R ) )
imasval.p 
|- .+ = ( +g ` R )
imasval.m 
|- .X. = ( .r ` R )
imasval.g 
|- G = ( Scalar ` R )
imasval.k 
|- K = ( Base ` G )
imasval.q 
|- .x. = ( .s ` R )
imasval.i 
|- ., = ( .i ` R )
imasval.j 
|- J = ( TopOpen ` R )
imasval.e 
|- E = ( dist ` R )
imasval.n 
|- N = ( le ` R )
imasval.a 
|- ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
imasval.t 
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
imasval.s 
|- ( ph -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
imasval.w 
|- ( ph -> I = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
imasval.o 
|- ( ph -> O = ( J qTop F ) )
imasval.d 
|- ( ph -> D = ( x e. B , y e. B |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) ) )
imasval.l 
|- ( ph -> .<_ = ( ( F o. N ) o. `' F ) )
imasval.f 
|- ( ph -> F : V -onto-> B )
imasval.r 
|- ( ph -> R e. Z )
Assertion imasval 
|- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )

Proof

Step Hyp Ref Expression
1 imasval.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasval.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasval.p 
 |-  .+ = ( +g ` R )
4 imasval.m 
 |-  .X. = ( .r ` R )
5 imasval.g 
 |-  G = ( Scalar ` R )
6 imasval.k 
 |-  K = ( Base ` G )
7 imasval.q 
 |-  .x. = ( .s ` R )
8 imasval.i 
 |-  ., = ( .i ` R )
9 imasval.j 
 |-  J = ( TopOpen ` R )
10 imasval.e 
 |-  E = ( dist ` R )
11 imasval.n 
 |-  N = ( le ` R )
12 imasval.a 
 |-  ( ph -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
13 imasval.t 
 |-  ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
14 imasval.s 
 |-  ( ph -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
15 imasval.w 
 |-  ( ph -> I = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
16 imasval.o 
 |-  ( ph -> O = ( J qTop F ) )
17 imasval.d 
 |-  ( ph -> D = ( x e. B , y e. B |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) ) )
18 imasval.l 
 |-  ( ph -> .<_ = ( ( F o. N ) o. `' F ) )
19 imasval.f 
 |-  ( ph -> F : V -onto-> B )
20 imasval.r 
 |-  ( ph -> R e. Z )
21 df-imas 
 |-  "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) )
22 21 a1i 
 |-  ( ph -> "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) ) )
23 fvexd 
 |-  ( ( ph /\ ( f = F /\ r = R ) ) -> ( Base ` r ) e. _V )
24 simplrl 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> f = F )
25 24 rneqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = ran F )
26 forn 
 |-  ( F : V -onto-> B -> ran F = B )
27 19 26 syl 
 |-  ( ph -> ran F = B )
28 27 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran F = B )
29 25 28 eqtrd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran f = B )
30 29 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( Base ` ndx ) , ran f >. = <. ( Base ` ndx ) , B >. )
31 simplrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> r = R )
32 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` r ) = ( Base ` R ) )
33 simpr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = ( Base ` r ) )
34 2 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> V = ( Base ` R ) )
35 32 33 34 3eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> v = V )
36 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` p ) = ( F ` p ) )
37 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` q ) = ( F ` q ) )
38 36 37 opeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( f ` p ) , ( f ` q ) >. = <. ( F ` p ) , ( F ` q ) >. )
39 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = ( +g ` R ) )
40 39 3 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( +g ` r ) = .+ )
41 40 oveqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( +g ` r ) q ) = ( p .+ q ) )
42 24 41 fveq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( +g ` r ) q ) ) = ( F ` ( p .+ q ) ) )
43 38 42 opeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. )
44 43 sneqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
45 35 44 iuneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
46 35 45 iuneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
47 12 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .+b = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .+ q ) ) >. } )
48 46 47 eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } = .+b )
49 48 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. = <. ( +g ` ndx ) , .+b >. )
50 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = ( .r ` R ) )
51 50 4 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .r ` r ) = .X. )
52 51 oveqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .r ` r ) q ) = ( p .X. q ) )
53 24 52 fveq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .r ` r ) q ) ) = ( F ` ( p .X. q ) ) )
54 38 53 opeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. )
55 54 sneqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
56 35 55 iuneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
57 35 56 iuneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
58 13 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .X. q ) ) >. } )
59 57 58 eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } = .xb )
60 59 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. = <. ( .r ` ndx ) , .xb >. )
61 30 49 60 tpeq123d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } )
62 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Scalar ` r ) = ( Scalar ` R ) )
63 62 5 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Scalar ` r ) = G )
64 63 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( Scalar ` ndx ) , ( Scalar ` r ) >. = <. ( Scalar ` ndx ) , G >. )
65 63 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` ( Scalar ` r ) ) = ( Base ` G ) )
66 65 6 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( Base ` ( Scalar ` r ) ) = K )
67 37 sneqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { ( f ` q ) } = { ( F ` q ) } )
68 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .s ` r ) = ( .s ` R ) )
69 68 7 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .s ` r ) = .x. )
70 69 oveqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .s ` r ) q ) = ( p .x. q ) )
71 24 70 fveq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( p ( .s ` r ) q ) ) = ( F ` ( p .x. q ) ) )
72 66 67 71 mpoeq123dv 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
73 72 iuneq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. V ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
74 35 iuneq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = U_ q e. V ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) )
75 14 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .(x) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) )
76 73 74 75 3eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) = .(x) )
77 76 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. = <. ( .s ` ndx ) , .(x) >. )
78 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .i ` r ) = ( .i ` R ) )
79 78 8 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( .i ` r ) = ., )
80 79 oveqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( p ( .i ` r ) q ) = ( p ., q ) )
81 38 80 opeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. = <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. )
82 81 sneqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
83 35 82 iuneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
84 35 83 iuneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
85 15 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> I = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ., q ) >. } )
86 84 85 eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } = I )
87 86 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. = <. ( .i ` ndx ) , I >. )
88 64 77 87 tpeq123d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } = { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } )
89 61 88 uneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) )
90 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( TopOpen ` r ) = ( TopOpen ` R ) )
91 90 9 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( TopOpen ` r ) = J )
92 91 24 oveq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( TopOpen ` r ) qTop f ) = ( J qTop F ) )
93 16 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> O = ( J qTop F ) )
94 92 93 eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( TopOpen ` r ) qTop f ) = O )
95 94 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. = <. ( TopSet ` ndx ) , O >. )
96 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( le ` r ) = ( le ` R ) )
97 96 11 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( le ` r ) = N )
98 24 97 coeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f o. ( le ` r ) ) = ( F o. N ) )
99 24 cnveqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> `' f = `' F )
100 98 99 coeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f o. ( le ` r ) ) o. `' f ) = ( ( F o. N ) o. `' F ) )
101 18 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> .<_ = ( ( F o. N ) o. `' F ) )
102 100 101 eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f o. ( le ` r ) ) o. `' f ) = .<_ )
103 102 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. = <. ( le ` ndx ) , .<_ >. )
104 35 sqxpeqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( v X. v ) = ( V X. V ) )
105 104 oveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( v X. v ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m ( 1 ... n ) ) )
106 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( h ` 1 ) ) ) )
107 106 eqeq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x <-> ( F ` ( 1st ` ( h ` 1 ) ) ) = x ) )
108 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( h ` n ) ) ) )
109 108 eqeq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 2nd ` ( h ` n ) ) ) = y <-> ( F ` ( 2nd ` ( h ` n ) ) ) = y ) )
110 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( h ` i ) ) ) )
111 24 fveq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) )
112 110 111 eqeq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) )
113 112 ralbidv 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) )
114 107 109 113 3anbi123d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) ) )
115 105 114 rabeqbidv 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } )
116 31 fveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( dist ` r ) = ( dist ` R ) )
117 116 10 eqtr4di 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( dist ` r ) = E )
118 117 coeq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( dist ` r ) o. g ) = ( E o. g ) )
119 118 oveq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( RR*s gsum ( ( dist ` r ) o. g ) ) = ( RR*s gsum ( E o. g ) ) )
120 115 119 mpteq12dv 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) = ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) )
121 120 rneqd 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) = ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) )
122 121 iuneq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) = U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) )
123 122 infeq1d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) = inf ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) )
124 29 29 123 mpoeq123dv 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) = ( x e. B , y e. B |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) ) )
125 17 ad2antrr 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> D = ( x e. B , y e. B |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) ) )
126 124 125 eqtr4d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) = D )
127 126 opeq2d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. = <. ( dist ` ndx ) , D >. )
128 95 103 127 tpeq123d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> { <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } = { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )
129 89 128 uneq12d 
 |-  ( ( ( ph /\ ( f = F /\ r = R ) ) /\ v = ( Base ` r ) ) -> ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
130 23 129 csbied 
 |-  ( ( ph /\ ( f = F /\ r = R ) ) -> [_ ( Base ` r ) / v ]_ ( ( { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` r ) >. , <. ( .s ` ndx ) , U_ q e. v ( p e. ( Base ` ( Scalar ` r ) ) , x e. { ( f ` q ) } |-> ( f ` ( p ( .s ` r ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( p ( .i ` r ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` r ) qTop f ) >. , <. ( le ` ndx ) , ( ( f o. ( le ` r ) ) o. `' f ) >. , <. ( dist ` ndx ) , ( x e. ran f , y e. ran f |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( v X. v ) ^m ( 1 ... n ) ) | ( ( f ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( f ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( f ` ( 2nd ` ( h ` i ) ) ) = ( f ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` r ) o. g ) ) ) , RR* , < ) ) >. } ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
131 fof 
 |-  ( F : V -onto-> B -> F : V --> B )
132 19 131 syl 
 |-  ( ph -> F : V --> B )
133 fvex 
 |-  ( Base ` R ) e. _V
134 2 133 eqeltrdi 
 |-  ( ph -> V e. _V )
135 132 134 fexd 
 |-  ( ph -> F e. _V )
136 20 elexd 
 |-  ( ph -> R e. _V )
137 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } e. _V
138 tpex 
 |-  { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } e. _V
139 137 138 unex 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) e. _V
140 tpex 
 |-  { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V
141 139 140 unex 
 |-  ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) e. _V
142 141 a1i 
 |-  ( ph -> ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) e. _V )
143 22 130 135 136 142 ovmpod 
 |-  ( ph -> ( F "s R ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )
144 1 143 eqtrd 
 |-  ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .xb >. } u. { <. ( Scalar ` ndx ) , G >. , <. ( .s ` ndx ) , .(x) >. , <. ( .i ` ndx ) , I >. } ) u. { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } ) )