Metamath Proof Explorer

Theorem prdsval

Description: Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by Mario Carneiro, 7-Jan-2017) (Revised by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Hypotheses prdsval.p 
|- P = ( S Xs_ R )
prdsval.k 
|- K = ( Base ` S )
prdsval.i 
|- ( ph -> dom R = I )
prdsval.b 
|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
prdsval.a 
|- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
prdsval.t 
|- ( ph -> .X. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
prdsval.m 
|- ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
prdsval.j 
|- ( ph -> ., = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
prdsval.o 
|- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )
prdsval.l 
|- ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
prdsval.d 
|- ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
prdsval.h 
|- ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
prdsval.x 
|- ( ph -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
prdsval.s 
|- ( ph -> S e. W )
prdsval.r 
|- ( ph -> R e. Z )
Assertion prdsval 
|- ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )

Proof

Step Hyp Ref Expression
1 prdsval.p 
 |-  P = ( S Xs_ R )
2 prdsval.k 
 |-  K = ( Base ` S )
3 prdsval.i 
 |-  ( ph -> dom R = I )
4 prdsval.b 
 |-  ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
5 prdsval.a 
 |-  ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
6 prdsval.t 
 |-  ( ph -> .X. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
7 prdsval.m 
 |-  ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
8 prdsval.j 
 |-  ( ph -> ., = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
9 prdsval.o 
 |-  ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )
10 prdsval.l 
 |-  ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
11 prdsval.d 
 |-  ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
12 prdsval.h 
 |-  ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
13 prdsval.x 
 |-  ( ph -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
14 prdsval.s 
 |-  ( ph -> S e. W )
15 prdsval.r 
 |-  ( ph -> R e. Z )
16 df-prds 
 |-  Xs_ = ( s e. _V , r e. _V |-> [_ X_ x e. dom r ( Base ` ( r ` x ) ) / v ]_ [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
17 16 a1i 
 |-  ( ph -> Xs_ = ( s e. _V , r e. _V |-> [_ X_ x e. dom r ( Base ` ( r ` x ) ) / v ]_ [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) ) )
18 vex 
 |-  r e. _V
19 18 rnex 
 |-  ran r e. _V
20 19 uniex 
 |-  U. ran r e. _V
21 20 rnex 
 |-  ran U. ran r e. _V
22 21 uniex 
 |-  U. ran U. ran r e. _V
23 baseid 
 |-  Base = Slot ( Base ` ndx )
24 23 strfvss 
 |-  ( Base ` ( r ` x ) ) C_ U. ran ( r ` x )
25 fvssunirn 
 |-  ( r ` x ) C_ U. ran r
26 rnss 
 |-  ( ( r ` x ) C_ U. ran r -> ran ( r ` x ) C_ ran U. ran r )
27 uniss 
 |-  ( ran ( r ` x ) C_ ran U. ran r -> U. ran ( r ` x ) C_ U. ran U. ran r )
28 25 26 27 mp2b 
 |-  U. ran ( r ` x ) C_ U. ran U. ran r
29 24 28 sstri 
 |-  ( Base ` ( r ` x ) ) C_ U. ran U. ran r
30 29 rgenw 
 |-  A. x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r
31 iunss 
 |-  ( U_ x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r <-> A. x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r )
32 30 31 mpbir 
 |-  U_ x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r
33 22 32 ssexi 
 |-  U_ x e. dom r ( Base ` ( r ` x ) ) e. _V
34 ixpssmap2g 
 |-  ( U_ x e. dom r ( Base ` ( r ` x ) ) e. _V -> X_ x e. dom r ( Base ` ( r ` x ) ) C_ ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) )
35 33 34 ax-mp 
 |-  X_ x e. dom r ( Base ` ( r ` x ) ) C_ ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r )
36 ovex 
 |-  ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) e. _V
37 36 ssex 
 |-  ( X_ x e. dom r ( Base ` ( r ` x ) ) C_ ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) -> X_ x e. dom r ( Base ` ( r ` x ) ) e. _V )
38 35 37 mp1i 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) e. _V )
39 simpr 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> r = R )
40 39 fveq1d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( r ` x ) = ( R ` x ) )
41 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( Base ` ( r ` x ) ) = ( Base ` ( R ` x ) ) )
42 41 ixpeq2dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. I ( Base ` ( r ` x ) ) = X_ x e. I ( Base ` ( R ` x ) ) )
43 39 dmeqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> dom r = dom R )
44 3 ad2antrr 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> dom R = I )
45 43 44 eqtrd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> dom r = I )
46 45 ixpeq1d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = X_ x e. I ( Base ` ( r ` x ) ) )
47 4 ad2antrr 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> B = X_ x e. I ( Base ` ( R ` x ) ) )
48 42 46 47 3eqtr4d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = B )
49 ovex 
 |-  ( U. ran U. ran U. ran r ^m dom r ) e. _V
50 ovssunirn 
 |-  ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran ( Hom ` ( r ` x ) )
51 df-hom 
 |-  Hom = Slot ; 1 4
52 51 strfvss 
 |-  ( Hom ` ( r ` x ) ) C_ U. ran ( r ` x )
53 52 28 sstri 
 |-  ( Hom ` ( r ` x ) ) C_ U. ran U. ran r
54 rnss 
 |-  ( ( Hom ` ( r ` x ) ) C_ U. ran U. ran r -> ran ( Hom ` ( r ` x ) ) C_ ran U. ran U. ran r )
55 uniss 
 |-  ( ran ( Hom ` ( r ` x ) ) C_ ran U. ran U. ran r -> U. ran ( Hom ` ( r ` x ) ) C_ U. ran U. ran U. ran r )
56 53 54 55 mp2b 
 |-  U. ran ( Hom ` ( r ` x ) ) C_ U. ran U. ran U. ran r
57 50 56 sstri 
 |-  ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran r
58 57 rgenw 
 |-  A. x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran r
59 ss2ixp 
 |-  ( A. x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran r -> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ X_ x e. dom r U. ran U. ran U. ran r )
60 58 59 ax-mp 
 |-  X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ X_ x e. dom r U. ran U. ran U. ran r
61 18 dmex 
 |-  dom r e. _V
62 22 rnex 
 |-  ran U. ran U. ran r e. _V
63 62 uniex 
 |-  U. ran U. ran U. ran r e. _V
64 61 63 ixpconst 
 |-  X_ x e. dom r U. ran U. ran U. ran r = ( U. ran U. ran U. ran r ^m dom r )
65 60 64 sseqtri 
 |-  X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) C_ ( U. ran U. ran U. ran r ^m dom r )
66 49 65 elpwi2 
 |-  X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran r ^m dom r )
67 66 rgen2w 
 |-  A. f e. v A. g e. v X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran r ^m dom r )
68 eqid 
 |-  ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) = ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) )
69 68 fmpo 
 |-  ( A. f e. v A. g e. v X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran r ^m dom r ) <-> ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) : ( v X. v ) --> ~P ( U. ran U. ran U. ran r ^m dom r ) )
70 67 69 mpbi 
 |-  ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) : ( v X. v ) --> ~P ( U. ran U. ran U. ran r ^m dom r )
71 vex 
 |-  v e. _V
72 71 71 xpex 
 |-  ( v X. v ) e. _V
73 49 pwex 
 |-  ~P ( U. ran U. ran U. ran r ^m dom r ) e. _V
74 fex2 
 |-  ( ( ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) : ( v X. v ) --> ~P ( U. ran U. ran U. ran r ^m dom r ) /\ ( v X. v ) e. _V /\ ~P ( U. ran U. ran U. ran r ^m dom r ) e. _V ) -> ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V )
75 70 72 73 74 mp3an 
 |-  ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V
76 75 a1i 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V )
77 simpr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> v = B )
78 45 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> dom r = I )
79 78 ixpeq1d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = X_ x e. I ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) )
80 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( Hom ` ( r ` x ) ) = ( Hom ` ( R ` x ) ) )
81 80 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
82 81 ixpeq2dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. I ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
83 82 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> X_ x e. I ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
84 79 83 eqtrd 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
85 77 77 84 mpoeq123dv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
86 12 ad3antrrr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
87 85 86 eqtr4d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) = H )
88 simplr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> v = B )
89 88 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Base ` ndx ) , v >. = <. ( Base ` ndx ) , B >. )
90 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( +g ` ( r ` x ) ) = ( +g ` ( R ` x ) ) )
91 90 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) )
92 45 91 mpteq12dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) )
93 92 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) )
94 77 77 93 mpoeq123dv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
95 94 adantr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
96 5 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
97 95 96 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) = .+ )
98 97 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. = <. ( +g ` ndx ) , .+ >. )
99 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( .r ` ( r ` x ) ) = ( .r ` ( R ` x ) ) )
100 99 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) )
101 45 100 mpteq12dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) )
102 101 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) )
103 77 77 102 mpoeq123dv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
104 103 adantr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
105 6 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> .X. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
106 104 105 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) = .X. )
107 106 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. = <. ( .r ` ndx ) , .X. >. )
108 89 98 107 tpeq123d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } )
109 simp-4r 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> s = S )
110 109 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Scalar ` ndx ) , s >. = <. ( Scalar ` ndx ) , S >. )
111 simpllr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> s = S )
112 111 fveq2d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = ( Base ` S ) )
113 112 2 eqtr4di 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = K )
114 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( .s ` ( r ` x ) ) = ( .s ` ( R ` x ) ) )
115 114 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) = ( f ( .s ` ( R ` x ) ) ( g ` x ) ) )
116 45 115 mpteq12dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) )
117 116 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) )
118 113 77 117 mpoeq123dv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
119 118 adantr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
120 7 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
121 119 120 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) = .x. )
122 121 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. = <. ( .s ` ndx ) , .x. >. )
123 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( .i ` ( r ` x ) ) = ( .i ` ( R ` x ) ) )
124 123 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) )
125 45 124 mpteq12dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) )
126 125 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) )
127 111 126 oveq12d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) = ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) )
128 77 77 127 mpoeq123dv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
129 128 adantr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
130 8 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ., = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
131 129 130 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) = ., )
132 131 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. = <. ( .i ` ndx ) , ., >. )
133 110 122 132 tpeq123d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } = { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )
134 108 133 uneq12d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
135 simpllr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> r = R )
136 135 coeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( TopOpen o. r ) = ( TopOpen o. R ) )
137 136 fveq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
138 9 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> O = ( Xt_ ` ( TopOpen o. R ) ) )
139 137 138 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = O )
140 139 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. = <. ( TopSet ` ndx ) , O >. )
141 77 sseq2d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( { f , g } C_ v <-> { f , g } C_ B ) )
142 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( le ` ( r ` x ) ) = ( le ` ( R ` x ) ) )
143 142 breqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
144 45 143 raleqbidv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
145 144 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
146 141 145 anbi12d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) <-> ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) ) )
147 146 opabbidv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
148 147 adantr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
149 10 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
150 148 149 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } = .<_ )
151 150 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. = <. ( le ` ndx ) , .<_ >. )
152 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( dist ` ( r ` x ) ) = ( dist ` ( R ` x ) ) )
153 152 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) )
154 45 153 mpteq12dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) )
155 154 adantr 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) )
156 155 rneqd 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) = ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) )
157 156 uneq1d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) = ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) )
158 157 supeq1d 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
159 77 77 158 mpoeq123dv 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
160 159 adantr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
161 11 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
162 160 161 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = D )
163 162 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. = <. ( dist ` ndx ) , D >. )
164 140 151 163 tpeq123d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } = { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } )
165 simpr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> h = H )
166 165 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , H >. )
167 88 sqxpeqd 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( v X. v ) = ( B X. B ) )
168 165 oveqd 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( c h ( 2nd ` a ) ) = ( c H ( 2nd ` a ) ) )
169 165 fveq1d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( h ` a ) = ( H ` a ) )
170 40 fveq2d 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( comp ` ( r ` x ) ) = ( comp ` ( R ` x ) ) )
171 170 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) = ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) )
172 171 oveqd 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) = ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) )
173 45 172 mpteq12dv 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) = ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) )
174 173 ad2antrr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) = ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) )
175 168 169 174 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) = ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) )
176 167 88 175 mpoeq123dv 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = ( a e. ( B X. B ) , c e. B |-> ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
177 13 ad4antr 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( c H ( 2nd ` a ) ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
178 176 177 eqtr4d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = .xb )
179 178 opeq2d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. = <. ( comp ` ndx ) , .xb >. )
180 166 179 preq12d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } = { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } )
181 164 180 uneq12d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) = ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) )
182 134 181 uneq12d 
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )
183 76 87 182 csbied2 
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )
184 38 48 183 csbied2 
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> [_ X_ x e. dom r ( Base ` ( r ` x ) ) / v ]_ [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )
185 184 anasss 
 |-  ( ( ph /\ ( s = S /\ r = R ) ) -> [_ X_ x e. dom r ( Base ` ( r ` x ) ) / v ]_ [_ ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) / h ]_ ( ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , s >. , <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsum ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )
186 14 elexd 
 |-  ( ph -> S e. _V )
187 15 elexd 
 |-  ( ph -> R e. _V )
188 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V
189 tpex 
 |-  { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V
190 188 189 unex 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V
191 tpex 
 |-  { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V
192 prex 
 |-  { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } e. _V
193 191 192 unex 
 |-  ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) e. _V
194 190 193 unex 
 |-  ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) e. _V
195 194 a1i 
 |-  ( ph -> ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) e. _V )
196 17 185 186 187 195 ovmpod 
 |-  ( ph -> ( S Xs_ R ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )
197 1 196 syl5eq 
 |-  ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) u. ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) ) )