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) (Revised by Zhi Wang, 18-Aug-2024)

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. ( ( 2nd ` a ) H c ) , 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. ( ( 2nd ` a ) H c ) , 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. ( ( 2nd ` a ) h c ) , 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. ( ( 2nd ` a ) h c ) , 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 prdsvallem
 |-  ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V
50 49 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 )
51 simpr
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> v = B )
52 45 adantr
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> dom r = I )
53 52 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 ) ) )
54 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( Hom ` ( r ` x ) ) = ( Hom ` ( R ` x ) ) )
55 54 oveqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
56 55 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 ) ) )
57 56 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 ) ) )
58 53 57 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 ) ) )
59 51 51 58 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 ) ) ) )
60 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 ) ) ) )
61 59 60 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 )
62 simplr
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> v = B )
63 62 opeq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Base ` ndx ) , v >. = <. ( Base ` ndx ) , B >. )
64 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( +g ` ( r ` x ) ) = ( +g ` ( R ` x ) ) )
65 64 oveqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) )
66 45 65 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 ) ) ) )
67 66 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 ) ) ) )
68 51 51 67 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 ) ) ) ) )
69 68 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 ) ) ) ) )
70 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 ) ) ) ) )
71 69 70 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 ) ) ) ) = .+ )
72 71 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 ) , .+ >. )
73 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( .r ` ( r ` x ) ) = ( .r ` ( R ` x ) ) )
74 73 oveqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) )
75 45 74 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 ) ) ) )
76 75 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 ) ) ) )
77 51 51 76 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 ) ) ) ) )
78 77 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 ) ) ) ) )
79 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 ) ) ) ) )
80 78 79 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. )
81 80 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. >. )
82 63 72 81 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. >. } )
83 simp-4r
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> s = S )
84 83 opeq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Scalar ` ndx ) , s >. = <. ( Scalar ` ndx ) , S >. )
85 simpllr
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> s = S )
86 85 fveq2d
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = ( Base ` S ) )
87 86 2 eqtr4di
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = K )
88 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( .s ` ( r ` x ) ) = ( .s ` ( R ` x ) ) )
89 88 oveqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) = ( f ( .s ` ( R ` x ) ) ( g ` x ) ) )
90 45 89 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 ) ) ) )
91 90 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 ) ) ) )
92 87 51 91 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 ) ) ) ) )
93 92 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 ) ) ) ) )
94 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 ) ) ) ) )
95 93 94 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. )
96 95 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. >. )
97 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( .i ` ( r ` x ) ) = ( .i ` ( R ` x ) ) )
98 97 oveqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) )
99 45 98 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 ) ) ) )
100 99 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 ) ) ) )
101 85 100 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 ) ) ) ) )
102 51 51 101 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 ) ) ) ) ) )
103 102 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 ) ) ) ) ) )
104 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 ) ) ) ) ) )
105 103 104 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 ) ) ) ) ) = ., )
106 105 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 ) , ., >. )
107 84 96 106 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 ) , ., >. } )
108 82 107 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 ) , ., >. } ) )
109 simpllr
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> r = R )
110 109 coeq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( TopOpen o. r ) = ( TopOpen o. R ) )
111 110 fveq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
112 9 ad4antr
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> O = ( Xt_ ` ( TopOpen o. R ) ) )
113 111 112 eqtr4d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = O )
114 113 opeq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. = <. ( TopSet ` ndx ) , O >. )
115 51 sseq2d
 |-  ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( { f , g } C_ v <-> { f , g } C_ B ) )
116 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( le ` ( r ` x ) ) = ( le ` ( R ` x ) ) )
117 116 breqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
118 45 117 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 ) ) )
119 118 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 ) ) )
120 115 119 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 ) ) ) )
121 120 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 ) ) } )
122 121 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 ) ) } )
123 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 ) ) } )
124 122 123 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 ) ) } = .<_ )
125 124 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 ) , .<_ >. )
126 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( dist ` ( r ` x ) ) = ( dist ` ( R ` x ) ) )
127 126 oveqd
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) )
128 45 127 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 ) ) ) )
129 128 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 ) ) ) )
130 129 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 ) ) ) )
131 130 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 } ) )
132 131 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* , < ) )
133 51 51 132 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* , < ) ) )
134 133 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* , < ) ) )
135 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* , < ) ) )
136 134 135 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 )
137 136 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 >. )
138 114 125 137 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 >. } )
139 simpr
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> h = H )
140 139 opeq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , H >. )
141 62 sqxpeqd
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( v X. v ) = ( B X. B ) )
142 139 oveqd
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( ( 2nd ` a ) h c ) = ( ( 2nd ` a ) H c ) )
143 139 fveq1d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( h ` a ) = ( H ` a ) )
144 40 fveq2d
 |-  ( ( ( ph /\ s = S ) /\ r = R ) -> ( comp ` ( r ` x ) ) = ( comp ` ( R ` x ) ) )
145 144 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 ) ) )
146 145 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 ) ) )
147 45 146 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 ) ) ) )
148 147 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 ) ) ) )
149 142 143 148 mpoeq123dv
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( d e. ( ( 2nd ` a ) h c ) , 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. ( ( 2nd ` a ) H c ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) )
150 141 62 149 mpoeq123dv
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( a e. ( v X. v ) , c e. v |-> ( d e. ( ( 2nd ` a ) h c ) , 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. ( ( 2nd ` a ) H c ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
151 13 ad4antr
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> .xb = ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) H c ) , e e. ( H ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
152 150 151 eqtr4d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( a e. ( v X. v ) , c e. v |-> ( d e. ( ( 2nd ` a ) h c ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = .xb )
153 152 opeq2d
 |-  ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( ( 2nd ` a ) h c ) , 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 >. )
154 140 153 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. ( ( 2nd ` a ) h c ) , 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 >. } )
155 138 154 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. ( ( 2nd ` a ) h c ) , 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 >. } ) )
156 108 155 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. ( ( 2nd ` a ) h c ) , 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 >. } ) ) )
157 50 61 156 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. ( ( 2nd ` a ) h c ) , 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 >. } ) ) )
158 38 48 157 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. ( ( 2nd ` a ) h c ) , 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 >. } ) ) )
159 158 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. ( ( 2nd ` a ) h c ) , 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 >. } ) ) )
160 14 elexd
 |-  ( ph -> S e. _V )
161 15 elexd
 |-  ( ph -> R e. _V )
162 tpex
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V
163 tpex
 |-  { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V
164 162 163 unex
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V
165 tpex
 |-  { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V
166 prex
 |-  { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } e. _V
167 165 166 unex
 |-  ( { <. ( TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .xb >. } ) e. _V
168 164 167 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
169 168 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 )
170 17 159 160 161 169 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 >. } ) ) )
171 1 170 eqtrid
 |-  ( 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 >. } ) ) )