Theorem prdsval 13507

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 13501	. . . 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 2818	. . . . . . . . . . . 12 |- r e. _V
5	4	rnex 5027	. . . . . . . . . . 11 |- ran r e. _V
6	5	uniex 4560	. . . . . . . . . 10 |- U. ran r e. _V
7	6	rnex 5027	. . . . . . . . 9 |- ran U. ran r e. _V
8	7	uniex 4560	. . . . . . . 8 |- U. ran U. ran r e. _V
9		baseid 13287	. . . . . . . . . . . . 13 |- Base = Slot ( Base ` ndx )
10		vex 2818	. . . . . . . . . . . . . . 15 |- x e. _V
11	4, 10	fvex 5692	. . . . . . . . . . . . . 14 |- ( r ` x ) e. _V
12	11	a1i 9	. . . . . . . . . . . . 13 |- ( T. -> ( r ` x ) e. _V )
13		basendxnn 13289	. . . . . . . . . . . . . 14 |- ( Base ` ndx ) e. NN
14	13	a1i 9	. . . . . . . . . . . . 13 |- ( T. -> ( Base ` ndx ) e. NN )
15	9, 12, 14	strfvssn 13255	. . . . . . . . . . . 12 |- ( T. -> ( Base ` ( r ` x ) ) C_ U. ran ( r ` x ) )
16	15	mptru 1407	. . . . . . . . . . 11 |- ( Base ` ( r ` x ) ) C_ U. ran ( r ` x )
17		fvssunirng 5687	. . . . . . . . . . . . 13 |- ( x e. _V -> ( r ` x ) C_ U. ran r )
18	17	elv 2819	. . . . . . . . . . . 12 |- ( r ` x ) C_ U. ran r
19		rnss 4989	. . . . . . . . . . . 12 |- ( ( r ` x ) C_ U. ran r -> ran ( r ` x ) C_ ran U. ran r )
20		uniss 3937	. . . . . . . . . . . 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 3249	. . . . . . . . . 10 |- ( Base ` ( r ` x ) ) C_ U. ran U. ran r
23	22	rgenw 2599	. . . . . . . . 9 |- A. x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r
24		iunss 4034	. . . . . . . . 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 4250	. . . . . . 7 |- U_ x e. dom r ( Base ` ( r ` x ) ) e. _V
27		ixpssmap2g 6964	. . . . . . 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 6891	. . . . . . . 8 |- ^m Fn ( _V X. _V )
30	4	dmex 5026	. . . . . . . 8 |- dom r e. _V
31		fnovex 6085	. . . . . . . 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 1374	. . . . . . 7 |- ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) e. _V
33	32	ssex 4249	. . . . . 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 5674	. . . . . . . 8 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( r ` x ) = ( R ` x ) )
37	36	fveq2d 5676	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( Base ` ( r ` x ) ) = ( Base ` ( R ` x ) ) )
38	37	ixpeq2dv 6951	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. I ( Base ` ( r ` x ) ) = X_ x e. I ( Base ` ( R ` x ) ) )
39	35	dmeqd 4960	. . . . . . . 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 2267	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ r = R ) -> dom r = I )
43	42	ixpeq1d 6947	. . . . . 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 2277	. . . . 5 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = B )
47		prdsvallem 13506	. . . . . . 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 6947	. . . . . . . . 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 5676	. . . . . . . . . . . 12 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( Hom ` ( r ` x ) ) = ( Hom ` ( R ` x ) ) )
53	52	oveqd 6069	. . . . . . . . . . 11 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
54	53	ixpeq2dv 6951	. . . . . . . . . 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 2267	. . . . . . . 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 6117	. . . . . . 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 2270	. . . . . 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 529	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> v = B )
62	61	opeq2d 3892	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Base ` ndx ) , v >. = <. ( Base ` ndx ) , B >. )
63	36	fveq2d 5676	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( +g ` ( r ` x ) ) = ( +g ` ( R ` x ) ) )
64	63	oveqd 6069	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) )
65	42, 64	mpteq12dv 4194	. . . . . . . . . . . . . 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 6117	. . . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 5676	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .r ` ( r ` x ) ) = ( .r ` ( R ` x ) ) )
74	73	oveqd 6069	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) )
75	42, 74	mpteq12dv 4194	. . . . . . . . . . . . . 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 6117	. . . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 3785	. . . . . . . 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 544	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> s = S )
85	84	opeq2d 3892	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. (Scalar ` ndx ) , s >. = <. (Scalar ` ndx ) , S >. )
86		simpllr 536	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> s = S )
87	86	fveq2d 5676	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = ( Base ` S ) )
88		prdsval.k	. . . . . . . . . . . . . 14 |- K = ( Base ` S )
89	87, 88	eqtr4di 2285	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = K )
90	36	fveq2d 5676	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .s ` ( r ` x ) ) = ( .s ` ( R ` x ) ) )
91	90	oveqd 6069	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) = ( f ( .s ` ( R ` x ) ) ( g ` x ) ) )
92	42, 91	mpteq12dv 4194	. . . . . . . . . . . . . 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 6117	. . . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 5676	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .i ` ( r ` x ) ) = ( .i ` ( R ` x ) ) )
101	100	oveqd 6069	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) )
102	42, 101	mpteq12dv 4194	. . . . . . . . . . . . . . 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 6070	. . . . . . . . . . . . 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 6117	. . . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 3785	. . . . . . . 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 3376	. . . . . . 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 536	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> r = R )
114	113	coeq2d 4919	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( TopOpen o. r ) = ( TopOpen o. R ) )
115	114	fveq2d 5676	. . . . . . . . . . 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 2270	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = O )
119	118	opeq2d 3892	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. = <. (TopSet ` ndx ) , O >. )
120	49	sseq2d 3270	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( { f , g } C_ v <-> { f , g } C_ B ) )
121	36	fveq2d 5676	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( le ` ( r ` x ) ) = ( le ` ( R ` x ) ) )
122	121	breqd 4122	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
123	42, 122	raleqbidv 2759	. . . . . . . . . . . . . . 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 4178	. . . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 5676	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( dist ` ( r ` x ) ) = ( dist ` ( R ` x ) ) )
133	132	oveqd 6069	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) )
134	42, 133	mpteq12dv 4194	. . . . . . . . . . . . . . . . 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 4988	. . . . . . . . . . . . . . 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 3374	. . . . . . . . . . . . . 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 7280	. . . . . . . . . . . . 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 6117	. . . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 3785	. . . . . . . 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 3892	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , H >. )
148	61	sqxpeqd 4777	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( v X. v ) = ( B X. B ) )
149	146	oveqd 6069	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( ( 2nd ` a ) h c ) = ( ( 2nd ` a ) H c ) )
150	146	fveq1d 5674	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( h ` a ) = ( H ` a ) )
151	36	fveq2d 5676	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> (comp ` ( r ` x ) ) = (comp ` ( R ` x ) ) )
152	151	oveqd 6069	. . . . . . . . . . . . . . . 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 6069	. . . . . . . . . . . . . . 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 4194	. . . . . . . . . . . . . 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 6117	. . . . . . . . . . . 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 6117	. . . . . . . . . . 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 2270	. . . . . . . . . 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 3892	. . . . . . . . 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 3778	. . . . . . . 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 3376	. . . . . . 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 3376	. . . . . 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 3188	. . . . 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 3188	. . . 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 2829	. . 3 |- ( ph -> S e. _V )
170		prdsval.r	. . . 4 |- ( ph -> R e. Z )
171	170	elexd 2829	. . 3 |- ( ph -> R e. _V )
172		dmexg 5023	. . . . . . . . . . 11 |- ( R e. Z -> dom R e. _V )
173	170, 172	syl 14	. . . . . . . . . 10 |- ( ph -> dom R e. _V )
174	40, 173	eqeltrrd 2312	. . . . . . . . 9 |- ( ph -> I e. _V )
175		basfn 13292	. . . . . . . . . . 11 |- Base Fn _V
176		fvexg 5691	. . . . . . . . . . . 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 5689	. . . . . . . . . . . 12 |- ( ( Fun Base /\ ( R ` x ) e. dom Base ) -> ( Base ` ( R ` x ) ) e. _V )
179	178	funfni 5460	. . . . . . . . . . 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 2618	. . . . . . . . 9 |- ( ph -> A. x e. I ( Base ` ( R ` x ) ) e. _V )
182		ixpexgg 6959	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> B e. _V )
185		opexg 4346	. . . . . . 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 13345	. . . . . . 7 |- ( +g ` ndx ) e. NN
188		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> .+ e. _V )
191		opexg 4346	. . . . . . 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 13366	. . . . . . . 8 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
194	193	simpri 113	. . . . . . 7 |- ( .r ` ndx ) e. NN
195		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> .X. e. _V )
198		opexg 4346	. . . . . . 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 4567	. . . . . 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 1274	. . . . 5 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V )
202		scaslid 13387	. . . . . . . 8 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
203	202	simpri 113	. . . . . . 7 |- (Scalar ` ndx ) e. NN
204		opexg 4346	. . . . . . 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 13397	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
207	206	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
208		funfvex 5689	. . . . . . . . . . . 12 |- ( ( Fun Base /\ S e. dom Base ) -> ( Base ` S ) e. _V )
209	208	funfni 5460	. . . . . . . . . . 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 2321	. . . . . . . . 9 |- ( ph -> K e. _V )
212		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> .x. e. _V )
215		opexg 4346	. . . . . . 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 13405	. . . . . . . 8 |- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
218	217	simpri 113	. . . . . . 7 |- ( .i ` ndx ) e. NN
219		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> ., e. _V )
222		opexg 4346	. . . . . . 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 4567	. . . . . 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 1274	. . . . 5 |- ( ph -> { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V )
226		unexg 4566	. . . . 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 13423	. . . . . . 7 |- (TopSet ` ndx ) e. NN
229		topnfn 13478	. . . . . . . . . . 11 |- TopOpen Fn _V
230		fnfun 5455	. . . . . . . . . . 11 |- ( TopOpen Fn _V -> Fun TopOpen )
231	229, 230	ax-mp 5	. . . . . . . . . 10 |- Fun TopOpen
232		cofunexg 6304	. . . . . . . . . 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 13498	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> O e. _V )
237		opexg 4346	. . . . . . 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 13437	. . . . . . 7 |- ( le ` ndx ) e. NN
240		vex 2818	. . . . . . . . . . . 12 |- f e. _V
241		vex 2818	. . . . . . . . . . . 12 |- g e. _V
242	240, 241	prss 3852	. . . . . . . . . . 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 4179	. . . . . . . . 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 4866	. . . . . . . . . . 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 4826	. . . . . . . . . . 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 4252	. . . . . . . . 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 2322	. . . . . . . 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 2311	. . . . . . 7 |- ( ph -> .<_ e. _V )
252		opexg 4346	. . . . . . 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 13452	. . . . . . 7 |- ( dist ` ndx ) e. NN
255		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> D e. _V )
258		opexg 4346	. . . . . . 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 4567	. . . . . 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 1274	. . . . 5 |- ( ph -> { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V )
262		homslid 13469	. . . . . . . 8 |- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
263	262	simpri 113	. . . . . . 7 |- ( Hom ` ndx ) e. NN
264		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> H e. _V )
267		opexg 4346	. . . . . . 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 13472	. . . . . . . 8 |- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
270	269	simpri 113	. . . . . . 7 |- (comp ` ndx ) e. NN
271		mpoexga 6410	. . . . . . . . 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 2311	. . . . . . 7 |- ( ph -> .xb e. _V )
274		opexg 4346	. . . . . . 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 4327	. . . . . 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 4566	. . . . 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 4566	. . . 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 6183	. 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 2279	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 1398   T. wtru 1399   e. wcel 2205   A.wral 2522   _Vcvv 2815   [_csb 3140   u. cun 3211   C_ wss 3213   {csn 3691   {cpr 3692   {ctp 3693   <.cop 3694   U.cuni 3916   U_ciun 3993   class class class wbr 4111   {copab 4172   |-> cmpt 4173   X. cxp 4749   dom cdm 4751   ran crn 4752   o. ccom 4755   Fun wfun 5348   Fn wfn 5349   ` cfv 5354  (class class class)co 6052   e. cmpo 6054   1stc1st 6334   2ndc2nd 6335   ^m cmap 6884   X_cixp 6935   supcsup 7275   0cc0 8132   RR*cxr 8312   < clt 8313   NNcn 9242   ndxcnx 13230  Slot cslot 13232   Basecbs 13233   +g cplusg 13311   .rcmulr 13312  Scalarcsca 13314   .scvsca 13315   .icip 13316  TopSetcts 13317   lecple 13318   distcds 13320   Hom chom 13322  compcco 13323   TopOpenctopn 13474   Xt_cpt 13489   gsum_g cgsu 13491   X__scprds 13499

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4227  ax-sep 4230  ax-pow 4289  ax-pr 4324  ax-un 4556  ax-setind 4661  ax-cnex 8223  ax-resscn 8224  ax-1cn 8225  ax-1re 8226  ax-icn 8227  ax-addcl 8228  ax-addrcl 8229  ax-mulcl 8230  ax-addcom 8232  ax-mulcom 8233  ax-addass 8234  ax-mulass 8235  ax-distr 8236  ax-i2m1 8237  ax-1rid 8239  ax-0id 8240  ax-rnegex 8241  ax-cnre 8243

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3045  df-csb 3141  df-dif 3215  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-tp 3699  df-op 3700  df-uni 3917  df-int 3952  df-iun 3995  df-br 4112  df-opab 4174  df-mpt 4175  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-res 4763  df-ima 4764  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-f1 5359  df-fo 5360  df-f1o 5361  df-fv 5362  df-riota 6005  df-ov 6055  df-oprab 6056  df-mpo 6057  df-1st 6336  df-2nd 6337  df-map 6886  df-ixp 6936  df-sup 7277  df-sub 8451  df-inn 9243  df-2 9301  df-3 9302  df-4 9303  df-5 9304  df-6 9305  df-7 9306  df-8 9307  df-9 9308  df-n0 9502  df-dec 9716  df-ndx 13236  df-slot 13237  df-base 13239  df-plusg 13324  df-mulr 13325  df-sca 13327  df-vsca 13328  df-ip 13329  df-tset 13330  df-ple 13331  df-ds 13333  df-hom 13335  df-cco 13336  df-rest 13475  df-topn 13476  df-topgen 13494  df-pt 13495  df-prds 13501

This theorem is referenced by:  prdsbaslemss  13508  prdssca  13509  prdsbas  13510  prdsplusg  13511  prdsmulr  13512