Theorem prdsval 13272

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

Hypotheses

Ref	Expression
prdsval.p	|- P = ( S X_s 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 gsumg ( 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

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

Distinct variable groups:   a, c, d, e, f, g, B   H, a, c, d, e   x, a, ph, c, d, e, f, g   x, I   R, a, c, d, e, f, g, x   S, a, c, d, e, f, g, x   f, K, g

Allowed substitution hints:   B( x)   D( x, e, f, g, a, c, d)   P( x, e, f, g, a, c, d)   .+ ( x, e, f, g, a, c, d)   .xb ( x, e, f, g, a, c, d)   .x. ( x, e, f, g, a, c, d)   .X. ( x, e, f, g, a, c, d)   H( x, f, g)   ., ( x, e, f, g, a, c, d)   I( e, f, g, a, c, d)   K( x, e, a, c, d)   .<_ ( x, e, f, g, a, c, d)   O( x, e, f, g, a, c, d)   W( x, e, f, g, a, c, d)   Z( x, e, f, g, a, c, d)

Proof of Theorem prdsval

Dummy variables h r s v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prdsval.p	. 2 |- P = ( S X_s R )
2		df-prds 13266	. . . 4 |- X_s = ( 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 gsumg ( 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 ) ) ) ) ) >. } ) ) )
3	2	a1i 9	. . 3 |- ( ph -> X_s = ( 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 gsumg ( 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 ) ) ) ) ) >. } ) ) ) )
4		vex 2782	. . . . . . . . . . . 12 |- r e. _V
5	4	rnex 4968	. . . . . . . . . . 11 |- ran r e. _V
6	5	uniex 4505	. . . . . . . . . 10 |- U. ran r e. _V
7	6	rnex 4968	. . . . . . . . 9 |- ran U. ran r e. _V
8	7	uniex 4505	. . . . . . . 8 |- U. ran U. ran r e. _V
9		baseid 13052	. . . . . . . . . . . . 13 |- Base = Slot ( Base ` ndx )
10		vex 2782	. . . . . . . . . . . . . . 15 |- x e. _V
11	4, 10	fvex 5623	. . . . . . . . . . . . . 14 |- ( r ` x ) e. _V
12	11	a1i 9	. . . . . . . . . . . . 13 |- ( T. -> ( r ` x ) e. _V )
13		basendxnn 13054	. . . . . . . . . . . . . 14 |- ( Base ` ndx ) e. NN
14	13	a1i 9	. . . . . . . . . . . . 13 |- ( T. -> ( Base ` ndx ) e. NN )
15	9, 12, 14	strfvssn 13020	. . . . . . . . . . . 12 |- ( T. -> ( Base ` ( r ` x ) ) C_ U. ran ( r ` x ) )
16	15	mptru 1384	. . . . . . . . . . 11 |- ( Base ` ( r ` x ) ) C_ U. ran ( r ` x )
17		fvssunirng 5618	. . . . . . . . . . . . 13 |- ( x e. _V -> ( r ` x ) C_ U. ran r )
18	17	elv 2783	. . . . . . . . . . . 12 |- ( r ` x ) C_ U. ran r
19		rnss 4930	. . . . . . . . . . . 12 |- ( ( r ` x ) C_ U. ran r -> ran ( r ` x ) C_ ran U. ran r )
20		uniss 3888	. . . . . . . . . . . 12 |- ( ran ( r ` x ) C_ ran U. ran r -> U. ran ( r ` x ) C_ U. ran U. ran r )
21	18, 19, 20	mp2b 8	. . . . . . . . . . 11 |- U. ran ( r ` x ) C_ U. ran U. ran r
22	16, 21	sstri 3213	. . . . . . . . . 10 |- ( Base ` ( r ` x ) ) C_ U. ran U. ran r
23	22	rgenw 2565	. . . . . . . . 9 |- A. x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r
24		iunss 3985	. . . . . . . . 9 |- ( 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 )
25	23, 24	mpbir 146	. . . . . . . 8 |- U_ x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r
26	8, 25	ssexi 4201	. . . . . . 7 |- U_ x e. dom r ( Base ` ( r ` x ) ) e. _V
27		ixpssmap2g 6844	. . . . . . 7 |- ( 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 ) )
28	26, 27	ax-mp 5	. . . . . 6 |- X_ x e. dom r ( Base ` ( r ` x ) ) C_ ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r )
29		fnmap 6772	. . . . . . . 8 |- ^m Fn ( _V X. _V )
30	4	dmex 4967	. . . . . . . 8 |- dom r e. _V
31		fnovex 6007	. . . . . . . 8 |- ( ( ^m Fn ( _V X. _V ) /\ U_ x e. dom r ( Base ` ( r ` x ) ) e. _V /\ dom r e. _V ) -> ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) e. _V )
32	29, 26, 30, 31	mp3an 1352	. . . . . . 7 |- ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) e. _V
33	32	ssex 4200	. . . . . 6 |- ( 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 )
34	28, 33	mp1i 10	. . . . 5 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) e. _V )
35		simpr 110	. . . . . . . . 9 |- ( ( ( ph /\ s = S ) /\ r = R ) -> r = R )
36	35	fveq1d 5605	. . . . . . . 8 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( r ` x ) = ( R ` x ) )
37	36	fveq2d 5607	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( Base ` ( r ` x ) ) = ( Base ` ( R ` x ) ) )
38	37	ixpeq2dv 6831	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. I ( Base ` ( r ` x ) ) = X_ x e. I ( Base ` ( R ` x ) ) )
39	35	dmeqd 4902	. . . . . . . 8 |- ( ( ( ph /\ s = S ) /\ r = R ) -> dom r = dom R )
40		prdsval.i	. . . . . . . . 9 |- ( ph -> dom R = I )
41	40	ad2antrr 488	. . . . . . . 8 |- ( ( ( ph /\ s = S ) /\ r = R ) -> dom R = I )
42	39, 41	eqtrd 2242	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ r = R ) -> dom r = I )
43	42	ixpeq1d 6827	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = X_ x e. I ( Base ` ( r ` x ) ) )
44		prdsval.b	. . . . . . 7 |- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) )
45	44	ad2antrr 488	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ r = R ) -> B = X_ x e. I ( Base ` ( R ` x ) ) )
46	38, 43, 45	3eqtr4d 2252	. . . . 5 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = B )
47		prdsvallem 13271	. . . . . . 7 |- ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) ) e. _V
48	47	a1i 9	. . . . . 6 |- ( ( ( ( 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 )
49		simpr 110	. . . . . . . 8 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> v = B )
50	42	adantr 276	. . . . . . . . . 10 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> dom r = I )
51	50	ixpeq1d 6827	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
52	36	fveq2d 5607	. . . . . . . . . . . 12 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( Hom ` ( r ` x ) ) = ( Hom ` ( R ` x ) ) )
53	52	oveqd 5991	. . . . . . . . . . 11 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
54	53	ixpeq2dv 6831	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
55	54	adantr 276	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
56	51, 55	eqtrd 2242	. . . . . . . 8 |- ( ( ( ( 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 ) ) )
57	49, 49, 56	mpoeq123dv 6037	. . . . . . 7 |- ( ( ( ( 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 ) ) ) )
58		prdsval.h	. . . . . . . 8 |- ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
59	58	ad3antrrr 492	. . . . . . 7 |- ( ( ( ( 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 ) ) ) )
60	57, 59	eqtr4d 2245	. . . . . 6 |- ( ( ( ( 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 )
61		simplr 528	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> v = B )
62	61	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Base ` ndx ) , v >. = <. ( Base ` ndx ) , B >. )
63	36	fveq2d 5607	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( +g ` ( r ` x ) ) = ( +g ` ( R ` x ) ) )
64	63	oveqd 5991	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) )
65	42, 64	mpteq12dv 4145	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) )
66	65	adantr 276	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
67	49, 49, 66	mpoeq123dv 6037	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) ) )
68	67	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) )
69		prdsval.a	. . . . . . . . . . . 12 |- ( ph -> .+ = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
70	69	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( 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	68, 70	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( 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 3843	. . . . . . . . 9 |- ( ( ( ( ( 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	36	fveq2d 5607	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .r ` ( r ` x ) ) = ( .r ` ( R ` x ) ) )
74	73	oveqd 5991	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) )
75	42, 74	mpteq12dv 4145	. . . . . . . . . . . . . 14 |- ( ( ( 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 276	. . . . . . . . . . . . 13 |- ( ( ( ( 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	49, 49, 76	mpoeq123dv 6037	. . . . . . . . . . . 12 |- ( ( ( ( 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 276	. . . . . . . . . . 11 |- ( ( ( ( ( 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		prdsval.t	. . . . . . . . . . . 12 |- ( ph -> .X. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
80	79	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) )
81	78, 80	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( 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. )
82	81	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( 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. >. )
83	62, 72, 82	tpeq123d 3738	. . . . . . . 8 |- ( ( ( ( ( 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. >. } )
84		simp-4r 542	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> s = S )
85	84	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. (Scalar ` ndx ) , s >. = <. (Scalar ` ndx ) , S >. )
86		simpllr 534	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> s = S )
87	86	fveq2d 5607	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = ( Base ` S ) )
88		prdsval.k	. . . . . . . . . . . . . 14 |- K = ( Base ` S )
89	87, 88	eqtr4di 2260	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = K )
90	36	fveq2d 5607	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .s ` ( r ` x ) ) = ( .s ` ( R ` x ) ) )
91	90	oveqd 5991	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) = ( f ( .s ` ( R ` x ) ) ( g ` x ) ) )
92	42, 91	mpteq12dv 4145	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) = ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) )
93	92	adantr 276	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
94	89, 49, 93	mpoeq123dv 6037	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) ) )
95	94	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) )
96		prdsval.m	. . . . . . . . . . . 12 |- ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
97	96	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) )
98	95, 97	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( 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. )
99	98	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( 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. >. )
100	36	fveq2d 5607	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .i ` ( r ` x ) ) = ( .i ` ( R ` x ) ) )
101	100	oveqd 5991	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) )
102	42, 101	mpteq12dv 4145	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
103	102	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) )
104	86, 103	oveq12d 5992	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) = ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) )
105	49, 49, 104	mpoeq123dv 6037	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) = ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
106	105	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) = ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
107		prdsval.j	. . . . . . . . . . . 12 |- ( ph -> ., = ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
108	107	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ., = ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
109	106, 108	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) = ., )
110	109	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. = <. ( .i ` ndx ) , ., >. )
111	85, 99, 110	tpeq123d 3738	. . . . . . . 8 |- ( ( ( ( ( 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 gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >. } = { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } )
112	83, 111	uneq12d 3339	. . . . . . 7 |- ( ( ( ( ( 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 gsumg ( 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 ) , ., >. } ) )
113		simpllr 534	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> r = R )
114	113	coeq2d 4861	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( TopOpen o. r ) = ( TopOpen o. R ) )
115	114	fveq2d 5607	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
116		prdsval.o	. . . . . . . . . . . 12 |- ( ph -> O = ( Xt_ ` ( TopOpen o. R ) ) )
117	116	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> O = ( Xt_ ` ( TopOpen o. R ) ) )
118	115, 117	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = O )
119	118	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. = <. (TopSet ` ndx ) , O >. )
120	49	sseq2d 3234	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( { f , g } C_ v <-> { f , g } C_ B ) )
121	36	fveq2d 5607	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( le ` ( r ` x ) ) = ( le ` ( R ` x ) ) )
122	121	breqd 4073	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
123	42, 122	raleqbidv 2724	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
124	123	adantr 276	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) )
125	120, 124	anbi12d 473	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
126	125	opabbidv 4129	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) } )
127	126	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) } )
128		prdsval.l	. . . . . . . . . . . 12 |- ( ph -> .<_ = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
129	128	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) } )
130	127, 129	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) } = .<_ )
131	130	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( 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 ) , .<_ >. )
132	36	fveq2d 5607	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( dist ` ( r ` x ) ) = ( dist ` ( R ` x ) ) )
133	132	oveqd 5991	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) )
134	42, 133	mpteq12dv 4145	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) ) )
135	134	adantr 276	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) ) )
136	135	rneqd 4929	. . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) ) )
137	136	uneq1d 3337	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 } ) )
138	137	supeq1d 7122	. . . . . . . . . . . . 13 |- ( ( ( ( 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* , < ) )
139	49, 49, 138	mpoeq123dv 6037	. . . . . . . . . . . 12 |- ( ( ( ( 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* , < ) ) )
140	139	adantr 276	. . . . . . . . . . 11 |- ( ( ( ( ( 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* , < ) ) )
141		prdsval.d	. . . . . . . . . . . 12 |- ( ph -> D = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
142	141	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( 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* , < ) ) )
143	140, 142	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( 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 )
144	143	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( 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 >. )
145	119, 131, 144	tpeq123d 3738	. . . . . . . 8 |- ( ( ( ( ( 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 >. } )
146		simpr 110	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> h = H )
147	146	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , H >. )
148	61	sqxpeqd 4722	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( v X. v ) = ( B X. B ) )
149	146	oveqd 5991	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( ( 2nd ` a ) h c ) = ( ( 2nd ` a ) H c ) )
150	146	fveq1d 5605	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( h ` a ) = ( H ` a ) )
151	36	fveq2d 5607	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> (comp ` ( r ` x ) ) = (comp ` ( R ` x ) ) )
152	151	oveqd 5991	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
153	152	oveqd 5991	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) )
154	42, 153	mpteq12dv 4145	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) )
155	154	ad2antrr 488	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) ) ) )
156	149, 150, 155	mpoeq123dv 6037	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) ) ) )
157	148, 61, 156	mpoeq123dv 6037	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) ) )
158		prdsval.x	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
159	158	ad4antr 494	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) ) )
160	157, 159	eqtr4d 2245	. . . . . . . . . 10 |- ( ( ( ( ( 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 )
161	160	opeq2d 3843	. . . . . . . . 9 |- ( ( ( ( ( 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 >. )
162	147, 161	preq12d 3731	. . . . . . . 8 |- ( ( ( ( ( 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 >. } )
163	145, 162	uneq12d 3339	. . . . . . 7 |- ( ( ( ( ( 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 >. } ) )
164	112, 163	uneq12d 3339	. . . . . 6 |- ( ( ( ( ( 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 gsumg ( 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 >. } ) ) )
165	48, 60, 164	csbied2 3152	. . . . 5 |- ( ( ( ( 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 gsumg ( 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 >. } ) ) )
166	34, 46, 165	csbied2 3152	. . . 4 |- ( ( ( 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 gsumg ( 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 >. } ) ) )
167	166	anasss 399	. . 3 |- ( ( 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 gsumg ( 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 >. } ) ) )
168		prdsval.s	. . . 4 |- ( ph -> S e. W )
169	168	elexd 2793	. . 3 |- ( ph -> S e. _V )
170		prdsval.r	. . . 4 |- ( ph -> R e. Z )
171	170	elexd 2793	. . 3 |- ( ph -> R e. _V )
172		dmexg 4964	. . . . . . . . . . 11 |- ( R e. Z -> dom R e. _V )
173	170, 172	syl 14	. . . . . . . . . 10 |- ( ph -> dom R e. _V )
174	40, 173	eqeltrrd 2287	. . . . . . . . 9 |- ( ph -> I e. _V )
175		basfn 13057	. . . . . . . . . . 11 |- Base Fn _V
176		fvexg 5622	. . . . . . . . . . . 12 |- ( ( R e. Z /\ x e. _V ) -> ( R ` x ) e. _V )
177	170, 10, 176	sylancl 413	. . . . . . . . . . 11 |- ( ph -> ( R ` x ) e. _V )
178		funfvex 5620	. . . . . . . . . . . 12 |- ( ( Fun Base /\ ( R ` x ) e. dom Base ) -> ( Base ` ( R ` x ) ) e. _V )
179	178	funfni 5399	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ ( R ` x ) e. _V ) -> ( Base ` ( R ` x ) ) e. _V )
180	175, 177, 179	sylancr 414	. . . . . . . . . 10 |- ( ph -> ( Base ` ( R ` x ) ) e. _V )
181	180	ralrimivw 2584	. . . . . . . . 9 |- ( ph -> A. x e. I ( Base ` ( R ` x ) ) e. _V )
182		ixpexgg 6839	. . . . . . . . 9 |- ( ( I e. _V /\ A. x e. I ( Base ` ( R ` x ) ) e. _V ) -> X_ x e. I ( Base ` ( R ` x ) ) e. _V )
183	174, 181, 182	syl2anc 411	. . . . . . . 8 |- ( ph -> X_ x e. I ( Base ` ( R ` x ) ) e. _V )
184	44, 183	eqeltrd 2286	. . . . . . 7 |- ( ph -> B e. _V )
185		opexg 4293	. . . . . . 7 |- ( ( ( Base ` ndx ) e. NN /\ B e. _V ) -> <. ( Base ` ndx ) , B >. e. _V )
186	13, 184, 185	sylancr 414	. . . . . 6 |- ( ph -> <. ( Base ` ndx ) , B >. e. _V )
187		plusgndxnn 13110	. . . . . . 7 |- ( +g ` ndx ) e. NN
188		mpoexga 6328	. . . . . . . . 9 |- ( ( B e. _V /\ B e. _V ) -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
189	184, 184, 188	syl2anc 411	. . . . . . . 8 |- ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
190	69, 189	eqeltrd 2286	. . . . . . 7 |- ( ph -> .+ e. _V )
191		opexg 4293	. . . . . . 7 |- ( ( ( +g ` ndx ) e. NN /\ .+ e. _V ) -> <. ( +g ` ndx ) , .+ >. e. _V )
192	187, 190, 191	sylancr 414	. . . . . 6 |- ( ph -> <. ( +g ` ndx ) , .+ >. e. _V )
193		mulrslid 13131	. . . . . . . 8 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
194	193	simpri 113	. . . . . . 7 |- ( .r ` ndx ) e. NN
195		mpoexga 6328	. . . . . . . . 9 |- ( ( B e. _V /\ B e. _V ) -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
196	184, 184, 195	syl2anc 411	. . . . . . . 8 |- ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
197	79, 196	eqeltrd 2286	. . . . . . 7 |- ( ph -> .X. e. _V )
198		opexg 4293	. . . . . . 7 |- ( ( ( .r ` ndx ) e. NN /\ .X. e. _V ) -> <. ( .r ` ndx ) , .X. >. e. _V )
199	194, 197, 198	sylancr 414	. . . . . 6 |- ( ph -> <. ( .r ` ndx ) , .X. >. e. _V )
200		tpexg 4512	. . . . . 6 |- ( ( <. ( Base ` ndx ) , B >. e. _V /\ <. ( +g ` ndx ) , .+ >. e. _V /\ <. ( .r ` ndx ) , .X. >. e. _V ) -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V )
201	186, 192, 199, 200	syl3anc 1252	. . . . 5 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V )
202		scaslid 13152	. . . . . . . 8 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
203	202	simpri 113	. . . . . . 7 |- (Scalar ` ndx ) e. NN
204		opexg 4293	. . . . . . 7 |- ( ( (Scalar ` ndx ) e. NN /\ S e. W ) -> <. (Scalar ` ndx ) , S >. e. _V )
205	203, 168, 204	sylancr 414	. . . . . 6 |- ( ph -> <. (Scalar ` ndx ) , S >. e. _V )
206		vscaslid 13162	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
207	206	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
208		funfvex 5620	. . . . . . . . . . . 12 |- ( ( Fun Base /\ S e. dom Base ) -> ( Base ` S ) e. _V )
209	208	funfni 5399	. . . . . . . . . . 11 |- ( ( Base Fn _V /\ S e. _V ) -> ( Base ` S ) e. _V )
210	175, 169, 209	sylancr 414	. . . . . . . . . 10 |- ( ph -> ( Base ` S ) e. _V )
211	88, 210	eqeltrid 2296	. . . . . . . . 9 |- ( ph -> K e. _V )
212		mpoexga 6328	. . . . . . . . 9 |- ( ( K e. _V /\ B e. _V ) -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
213	211, 184, 212	syl2anc 411	. . . . . . . 8 |- ( ph -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
214	96, 213	eqeltrd 2286	. . . . . . 7 |- ( ph -> .x. e. _V )
215		opexg 4293	. . . . . . 7 |- ( ( ( .s ` ndx ) e. NN /\ .x. e. _V ) -> <. ( .s ` ndx ) , .x. >. e. _V )
216	207, 214, 215	sylancr 414	. . . . . 6 |- ( ph -> <. ( .s ` ndx ) , .x. >. e. _V )
217		ipslid 13170	. . . . . . . 8 |- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
218	217	simpri 113	. . . . . . 7 |- ( .i ` ndx ) e. NN
219		mpoexga 6328	. . . . . . . . 9 |- ( ( B e. _V /\ B e. _V ) -> ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) e. _V )
220	184, 184, 219	syl2anc 411	. . . . . . . 8 |- ( ph -> ( f e. B , g e. B |-> ( S gsumg ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) e. _V )
221	107, 220	eqeltrd 2286	. . . . . . 7 |- ( ph -> ., e. _V )
222		opexg 4293	. . . . . . 7 |- ( ( ( .i ` ndx ) e. NN /\ ., e. _V ) -> <. ( .i ` ndx ) , ., >. e. _V )
223	218, 221, 222	sylancr 414	. . . . . 6 |- ( ph -> <. ( .i ` ndx ) , ., >. e. _V )
224		tpexg 4512	. . . . . 6 |- ( ( <. (Scalar ` ndx ) , S >. e. _V /\ <. ( .s ` ndx ) , .x. >. e. _V /\ <. ( .i ` ndx ) , ., >. e. _V ) -> { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V )
225	205, 216, 223, 224	syl3anc 1252	. . . . 5 |- ( ph -> { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V )
226		unexg 4511	. . . . 5 |- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V /\ { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V ) -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V )
227	201, 225, 226	syl2anc 411	. . . 4 |- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V )
228		tsetndxnn 13188	. . . . . . 7 |- (TopSet ` ndx ) e. NN
229		topnfn 13243	. . . . . . . . . . 11 |- TopOpen Fn _V
230		fnfun 5394	. . . . . . . . . . 11 |- ( TopOpen Fn _V -> Fun TopOpen )
231	229, 230	ax-mp 5	. . . . . . . . . 10 |- Fun TopOpen
232		cofunexg 6224	. . . . . . . . . 10 |- ( ( Fun TopOpen /\ R e. Z ) -> ( TopOpen o. R ) e. _V )
233	231, 170, 232	sylancr 414	. . . . . . . . 9 |- ( ph -> ( TopOpen o. R ) e. _V )
234		ptex 13263	. . . . . . . . 9 |- ( ( TopOpen o. R ) e. _V -> ( Xt_ ` ( TopOpen o. R ) ) e. _V )
235	233, 234	syl 14	. . . . . . . 8 |- ( ph -> ( Xt_ ` ( TopOpen o. R ) ) e. _V )
236	116, 235	eqeltrd 2286	. . . . . . 7 |- ( ph -> O e. _V )
237		opexg 4293	. . . . . . 7 |- ( ( (TopSet ` ndx ) e. NN /\ O e. _V ) -> <. (TopSet ` ndx ) , O >. e. _V )
238	228, 236, 237	sylancr 414	. . . . . 6 |- ( ph -> <. (TopSet ` ndx ) , O >. e. _V )
239		plendxnn 13202	. . . . . . 7 |- ( le ` ndx ) e. NN
240		vex 2782	. . . . . . . . . . . 12 |- f e. _V
241		vex 2782	. . . . . . . . . . . 12 |- g e. _V
242	240, 241	prss 3803	. . . . . . . . . . 11 |- ( ( f e. B /\ g e. B ) <-> { f , g } C_ B )
243	242	anbi1i 458	. . . . . . . . . 10 |- ( ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) <-> ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
244	243	opabbii 4130	. . . . . . . . 9 |- { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) }
245		xpexg 4810	. . . . . . . . . . 11 |- ( ( B e. _V /\ B e. _V ) -> ( B X. B ) e. _V )
246	184, 184, 245	syl2anc 411	. . . . . . . . . 10 |- ( ph -> ( B X. B ) e. _V )
247		opabssxp 4770	. . . . . . . . . . 11 |- { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } C_ ( B X. B )
248	247	a1i 9	. . . . . . . . . 10 |- ( ph -> { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } C_ ( B X. B ) )
249	246, 248	ssexd 4203	. . . . . . . . 9 |- ( ph -> { <. f , g >. | ( ( f e. B /\ g e. B ) /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } e. _V )
250	244, 249	eqeltrrid 2297	. . . . . . . 8 |- ( ph -> { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } e. _V )
251	128, 250	eqeltrd 2286	. . . . . . 7 |- ( ph -> .<_ e. _V )
252		opexg 4293	. . . . . . 7 |- ( ( ( le ` ndx ) e. NN /\ .<_ e. _V ) -> <. ( le ` ndx ) , .<_ >. e. _V )
253	239, 251, 252	sylancr 414	. . . . . 6 |- ( ph -> <. ( le ` ndx ) , .<_ >. e. _V )
254		dsndxnn 13217	. . . . . . 7 |- ( dist ` ndx ) e. NN
255		mpoexga 6328	. . . . . . . . 9 |- ( ( B e. _V /\ B e. _V ) -> ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) e. _V )
256	184, 184, 255	syl2anc 411	. . . . . . . 8 |- ( ph -> ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) e. _V )
257	141, 256	eqeltrd 2286	. . . . . . 7 |- ( ph -> D e. _V )
258		opexg 4293	. . . . . . 7 |- ( ( ( dist ` ndx ) e. NN /\ D e. _V ) -> <. ( dist ` ndx ) , D >. e. _V )
259	254, 257, 258	sylancr 414	. . . . . 6 |- ( ph -> <. ( dist ` ndx ) , D >. e. _V )
260		tpexg 4512	. . . . . 6 |- ( ( <. (TopSet ` ndx ) , O >. e. _V /\ <. ( le ` ndx ) , .<_ >. e. _V /\ <. ( dist ` ndx ) , D >. e. _V ) -> { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V )
261	238, 253, 259, 260	syl3anc 1252	. . . . 5 |- ( ph -> { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V )
262		homslid 13234	. . . . . . . 8 |- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
263	262	simpri 113	. . . . . . 7 |- ( Hom ` ndx ) e. NN
264		mpoexga 6328	. . . . . . . . 9 |- ( ( B e. _V /\ B e. _V ) -> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) e. _V )
265	184, 184, 264	syl2anc 411	. . . . . . . 8 |- ( ph -> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) e. _V )
266	58, 265	eqeltrd 2286	. . . . . . 7 |- ( ph -> H e. _V )
267		opexg 4293	. . . . . . 7 |- ( ( ( Hom ` ndx ) e. NN /\ H e. _V ) -> <. ( Hom ` ndx ) , H >. e. _V )
268	263, 266, 267	sylancr 414	. . . . . 6 |- ( ph -> <. ( Hom ` ndx ) , H >. e. _V )
269		ccoslid 13237	. . . . . . . 8 |- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
270	269	simpri 113	. . . . . . 7 |- (comp ` ndx ) e. NN
271		mpoexga 6328	. . . . . . . . 9 |- ( ( ( B X. B ) e. _V /\ B e. _V ) -> ( 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 ) ) ) ) ) e. _V )
272	246, 184, 271	syl2anc 411	. . . . . . . 8 |- ( ph -> ( 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 ) ) ) ) ) e. _V )
273	158, 272	eqeltrd 2286	. . . . . . 7 |- ( ph -> .xb e. _V )
274		opexg 4293	. . . . . . 7 |- ( ( (comp ` ndx ) e. NN /\ .xb e. _V ) -> <. (comp ` ndx ) , .xb >. e. _V )
275	270, 273, 274	sylancr 414	. . . . . 6 |- ( ph -> <. (comp ` ndx ) , .xb >. e. _V )
276		prexg 4274	. . . . . 6 |- ( ( <. ( Hom ` ndx ) , H >. e. _V /\ <. (comp ` ndx ) , .xb >. e. _V ) -> { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } e. _V )
277	268, 275, 276	syl2anc 411	. . . . 5 |- ( ph -> { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } e. _V )
278		unexg 4511	. . . . 5 |- ( ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V /\ { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } e. _V ) -> ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) e. _V )
279	261, 277, 278	syl2anc 411	. . . 4 |- ( ph -> ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) e. _V )
280		unexg 4511	. . . 4 |- ( ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) e. _V /\ ( { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } u. { <. ( Hom ` ndx ) , H >. , <. (comp ` ndx ) , .xb >. } ) e. _V ) -> ( ( { <. ( 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 )
281	227, 279, 280	syl2anc 411	. . 3 |- ( 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 )
282	3, 167, 169, 171, 281	ovmpod 6103	. 2 |- ( ph -> ( S X_s 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 >. } ) ) )
283	1, 282	eqtrid 2254	1 |- ( 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 >. } ) ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1375   T. wtru 1376   e. wcel 2180   A.wral 2488   _Vcvv 2779   [_csb 3104   u. cun 3175   C_ wss 3177   {csn 3646   {cpr 3647   {ctp 3648   <.cop 3649   U.cuni 3867   U_ciun 3944   class class class wbr 4062   {copab 4123   |-> cmpt 4124   X. cxp 4694   dom cdm 4696   ran crn 4697   o. ccom 4700   Fun wfun 5288   Fn wfn 5289   ` cfv 5294  (class class class)co 5974   e. cmpo 5976   1stc1st 6254   2ndc2nd 6255   ^m cmap 6765   X_cixp 6815   supcsup 7117   0cc0 7967   RR*cxr 8148   < clt 8149   NNcn 9078   ndxcnx 12995  Slot cslot 12997   Basecbs 12998   +g cplusg 13076   .rcmulr 13077  Scalarcsca 13079   .scvsca 13080   .icip 13081  TopSetcts 13082   lecple 13083   distcds 13085   Hom chom 13087  compcco 13088   TopOpenctopn 13239   Xt_cpt 13254   gsum_g cgsu 13256   X__scprds 13264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501  ax-setind 4606  ax-cnex 8058  ax-resscn 8059  ax-1cn 8060  ax-1re 8061  ax-icn 8062  ax-addcl 8063  ax-addrcl 8064  ax-mulcl 8065  ax-addcom 8067  ax-mulcom 8068  ax-addass 8069  ax-mulass 8070  ax-distr 8071  ax-i2m1 8072  ax-1rid 8074  ax-0id 8075  ax-rnegex 8076  ax-cnre 8078

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-fal 1381  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-tp 3654  df-op 3655  df-uni 3868  df-int 3903  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302  df-riota 5927  df-ov 5977  df-oprab 5978  df-mpo 5979  df-1st 6256  df-2nd 6257  df-map 6767  df-ixp 6816  df-sup 7119  df-sub 8287  df-inn 9079  df-2 9137  df-3 9138  df-4 9139  df-5 9140  df-6 9141  df-7 9142  df-8 9143  df-9 9144  df-n0 9338  df-dec 9547  df-ndx 13001  df-slot 13002  df-base 13004  df-plusg 13089  df-mulr 13090  df-sca 13092  df-vsca 13093  df-ip 13094  df-tset 13095  df-ple 13096  df-ds 13098  df-hom 13100  df-cco 13101  df-rest 13240  df-topn 13241  df-topgen 13259  df-pt 13260  df-prds 13266

This theorem is referenced by:  prdsbaslemss  13273  prdssca  13274  prdsbas  13275  prdsplusg  13276  prdsmulr  13277