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 >. } ) )