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