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