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