Theorem prdsval 12975

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 12969	. . . 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 2766	. . . . . . . . . . . 12 |- r e. _V
5	4	rnex 4934	. . . . . . . . . . 11 |- ran r e. _V
6	5	uniex 4473	. . . . . . . . . 10 |- U. ran r e. _V
7	6	rnex 4934	. . . . . . . . 9 |- ran U. ran r e. _V
8	7	uniex 4473	. . . . . . . 8 |- U. ran U. ran r e. _V
9		baseid 12757	. . . . . . . . . . . . 13 |- Base = Slot ( Base ` ndx )
10		vex 2766	. . . . . . . . . . . . . . 15 |- x e. _V
11	4, 10	fvex 5581	. . . . . . . . . . . . . 14 |- ( r ` x ) e. _V
12	11	a1i 9	. . . . . . . . . . . . 13 |- ( T. -> ( r ` x ) e. _V )
13		basendxnn 12759	. . . . . . . . . . . . . 14 |- ( Base ` ndx ) e. NN
14	13	a1i 9	. . . . . . . . . . . . 13 |- ( T. -> ( Base ` ndx ) e. NN )
15	9, 12, 14	strfvssn 12725	. . . . . . . . . . . 12 |- ( T. -> ( Base ` ( r ` x ) ) C_ U. ran ( r ` x ) )
16	15	mptru 1373	. . . . . . . . . . 11 |- ( Base ` ( r ` x ) ) C_ U. ran ( r ` x )
17		fvssunirng 5576	. . . . . . . . . . . . 13 |- ( x e. _V -> ( r ` x ) C_ U. ran r )
18	17	elv 2767	. . . . . . . . . . . 12 |- ( r ` x ) C_ U. ran r
19		rnss 4897	. . . . . . . . . . . 12 |- ( ( r ` x ) C_ U. ran r -> ran ( r ` x ) C_ ran U. ran r )
20		uniss 3861	. . . . . . . . . . . 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 3193	. . . . . . . . . 10 |- ( Base ` ( r ` x ) ) C_ U. ran U. ran r
23	22	rgenw 2552	. . . . . . . . 9 |- A. x e. dom r ( Base ` ( r ` x ) ) C_ U. ran U. ran r
24		iunss 3958	. . . . . . . . 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 4172	. . . . . . 7 |- U_ x e. dom r ( Base ` ( r ` x ) ) e. _V
27		ixpssmap2g 6795	. . . . . . 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 6723	. . . . . . . 8 |- ^m Fn ( _V X. _V )
30	4	dmex 4933	. . . . . . . 8 |- dom r e. _V
31		fnovex 5958	. . . . . . . 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 1348	. . . . . . 7 |- ( U_ x e. dom r ( Base ` ( r ` x ) ) ^m dom r ) e. _V
33	32	ssex 4171	. . . . . 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 5563	. . . . . . . 8 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( r ` x ) = ( R ` x ) )
37	36	fveq2d 5565	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( Base ` ( r ` x ) ) = ( Base ` ( R ` x ) ) )
38	37	ixpeq2dv 6782	. . . . . 6 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. I ( Base ` ( r ` x ) ) = X_ x e. I ( Base ` ( R ` x ) ) )
39	35	dmeqd 4869	. . . . . . . 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 2229	. . . . . . 7 |- ( ( ( ph /\ s = S ) /\ r = R ) -> dom r = I )
43	42	ixpeq1d 6778	. . . . . 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 2239	. . . . 5 |- ( ( ( ph /\ s = S ) /\ r = R ) -> X_ x e. dom r ( Base ` ( r ` x ) ) = B )
47		prdsvallem 12974	. . . . . . 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 6778	. . . . . . . . 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 5565	. . . . . . . . . . . 12 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( Hom ` ( r ` x ) ) = ( Hom ` ( R ` x ) ) )
53	52	oveqd 5942	. . . . . . . . . . 11 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) )
54	53	ixpeq2dv 6782	. . . . . . . . . 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 2229	. . . . . . . 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 5988	. . . . . . 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 2232	. . . . . 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 3816	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Base ` ndx ) , v >. = <. ( Base ` ndx ) , B >. )
63	36	fveq2d 5565	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( +g ` ( r ` x ) ) = ( +g ` ( R ` x ) ) )
64	63	oveqd 5942	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) )
65	42, 64	mpteq12dv 4116	. . . . . . . . . . . . . 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 5988	. . . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 5565	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .r ` ( r ` x ) ) = ( .r ` ( R ` x ) ) )
74	73	oveqd 5942	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) )
75	42, 74	mpteq12dv 4116	. . . . . . . . . . . . . 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 5988	. . . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 3715	. . . . . . . 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 3816	. . . . . . . . 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 5565	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = ( Base ` S ) )
88		prdsval.k	. . . . . . . . . . . . . 14 |- K = ( Base ` S )
89	87, 88	eqtr4di 2247	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( Base ` s ) = K )
90	36	fveq2d 5565	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .s ` ( r ` x ) ) = ( .s ` ( R ` x ) ) )
91	90	oveqd 5942	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) = ( f ( .s ` ( R ` x ) ) ( g ` x ) ) )
92	42, 91	mpteq12dv 4116	. . . . . . . . . . . . . 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 5988	. . . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 5565	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( .i ` ( r ` x ) ) = ( .i ` ( R ` x ) ) )
101	100	oveqd 5942	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) )
102	42, 101	mpteq12dv 4116	. . . . . . . . . . . . . . 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 5943	. . . . . . . . . . . . 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 5988	. . . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 3715	. . . . . . . 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 3319	. . . . . . 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 4829	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( TopOpen o. r ) = ( TopOpen o. R ) )
115	114	fveq2d 5565	. . . . . . . . . . 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 2232	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( Xt_ ` ( TopOpen o. r ) ) = O )
119	118	opeq2d 3816	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. = <. (TopSet ` ndx ) , O >. )
120	49	sseq2d 3214	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) -> ( { f , g } C_ v <-> { f , g } C_ B ) )
121	36	fveq2d 5565	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( le ` ( r ` x ) ) = ( le ` ( R ` x ) ) )
122	121	breqd 4045	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) <-> ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) )
123	42, 122	raleqbidv 2709	. . . . . . . . . . . . . . 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 4100	. . . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 5565	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( dist ` ( r ` x ) ) = ( dist ` ( R ` x ) ) )
133	132	oveqd 5942	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ s = S ) /\ r = R ) -> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) = ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) )
134	42, 133	mpteq12dv 4116	. . . . . . . . . . . . . . . . 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 4896	. . . . . . . . . . . . . . 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 3317	. . . . . . . . . . . . . 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 7062	. . . . . . . . . . . . 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 5988	. . . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 3715	. . . . . . . 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 3816	. . . . . . . . 9 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> <. ( Hom ` ndx ) , h >. = <. ( Hom ` ndx ) , H >. )
148	61	sqxpeqd 4690	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( v X. v ) = ( B X. B ) )
149	146	oveqd 5942	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( ( 2nd ` a ) h c ) = ( ( 2nd ` a ) H c ) )
150	146	fveq1d 5563	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ s = S ) /\ r = R ) /\ v = B ) /\ h = H ) -> ( h ` a ) = ( H ` a ) )
151	36	fveq2d 5565	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ s = S ) /\ r = R ) -> (comp ` ( r ` x ) ) = (comp ` ( R ` x ) ) )
152	151	oveqd 5942	. . . . . . . . . . . . . . . 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 5942	. . . . . . . . . . . . . . 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 4116	. . . . . . . . . . . . . 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 5988	. . . . . . . . . . . 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 5988	. . . . . . . . . . 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 2232	. . . . . . . . . 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 3816	. . . . . . . . 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 3708	. . . . . . . 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 3319	. . . . . . 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 3319	. . . . . 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 3132	. . . . 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 3132	. . . 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 2776	. . 3 |- ( ph -> S e. _V )
170		prdsval.r	. . . 4 |- ( ph -> R e. Z )
171	170	elexd 2776	. . 3 |- ( ph -> R e. _V )
172		dmexg 4931	. . . . . . . . . . 11 |- ( R e. Z -> dom R e. _V )
173	170, 172	syl 14	. . . . . . . . . 10 |- ( ph -> dom R e. _V )
174	40, 173	eqeltrrd 2274	. . . . . . . . 9 |- ( ph -> I e. _V )
175		basfn 12761	. . . . . . . . . . 11 |- Base Fn _V
176		fvexg 5580	. . . . . . . . . . . 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 5578	. . . . . . . . . . . 12 |- ( ( Fun Base /\ ( R ` x ) e. dom Base ) -> ( Base ` ( R ` x ) ) e. _V )
179	178	funfni 5361	. . . . . . . . . . 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 2571	. . . . . . . . 9 |- ( ph -> A. x e. I ( Base ` ( R ` x ) ) e. _V )
182		ixpexgg 6790	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> B e. _V )
185		opexg 4262	. . . . . . 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 12814	. . . . . . 7 |- ( +g ` ndx ) e. NN
188		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> .+ e. _V )
191		opexg 4262	. . . . . . 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 12834	. . . . . . . 8 |- ( .r = Slot ( .r ` ndx ) /\ ( .r ` ndx ) e. NN )
194	193	simpri 113	. . . . . . 7 |- ( .r ` ndx ) e. NN
195		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> .X. e. _V )
198		opexg 4262	. . . . . . 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 4480	. . . . . 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 1249	. . . . 5 |- ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } e. _V )
202		scaslid 12855	. . . . . . . 8 |- (Scalar = Slot (Scalar ` ndx ) /\ (Scalar ` ndx ) e. NN )
203	202	simpri 113	. . . . . . 7 |- (Scalar ` ndx ) e. NN
204		opexg 4262	. . . . . . 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 12865	. . . . . . . 8 |- ( .s = Slot ( .s ` ndx ) /\ ( .s ` ndx ) e. NN )
207	206	simpri 113	. . . . . . 7 |- ( .s ` ndx ) e. NN
208		funfvex 5578	. . . . . . . . . . . 12 |- ( ( Fun Base /\ S e. dom Base ) -> ( Base ` S ) e. _V )
209	208	funfni 5361	. . . . . . . . . . 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 2283	. . . . . . . . 9 |- ( ph -> K e. _V )
212		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> .x. e. _V )
215		opexg 4262	. . . . . . 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 12873	. . . . . . . 8 |- ( .i = Slot ( .i ` ndx ) /\ ( .i ` ndx ) e. NN )
218	217	simpri 113	. . . . . . 7 |- ( .i ` ndx ) e. NN
219		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> ., e. _V )
222		opexg 4262	. . . . . . 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 4480	. . . . . 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 1249	. . . . 5 |- ( ph -> { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } e. _V )
226		unexg 4479	. . . . 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 12891	. . . . . . 7 |- (TopSet ` ndx ) e. NN
229		topnfn 12946	. . . . . . . . . . 11 |- TopOpen Fn _V
230		fnfun 5356	. . . . . . . . . . 11 |- ( TopOpen Fn _V -> Fun TopOpen )
231	229, 230	ax-mp 5	. . . . . . . . . 10 |- Fun TopOpen
232		cofunexg 6175	. . . . . . . . . 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 12966	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> O e. _V )
237		opexg 4262	. . . . . . 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 12905	. . . . . . 7 |- ( le ` ndx ) e. NN
240		vex 2766	. . . . . . . . . . . 12 |- f e. _V
241		vex 2766	. . . . . . . . . . . 12 |- g e. _V
242	240, 241	prss 3779	. . . . . . . . . . 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 4101	. . . . . . . . 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 4778	. . . . . . . . . . 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 4738	. . . . . . . . . . 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 4174	. . . . . . . . 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 2284	. . . . . . . 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 2273	. . . . . . 7 |- ( ph -> .<_ e. _V )
252		opexg 4262	. . . . . . 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 12920	. . . . . . 7 |- ( dist ` ndx ) e. NN
255		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> D e. _V )
258		opexg 4262	. . . . . . 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 4480	. . . . . 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 1249	. . . . 5 |- ( ph -> { <. (TopSet ` ndx ) , O >. , <. ( le ` ndx ) , .<_ >. , <. ( dist ` ndx ) , D >. } e. _V )
262		homslid 12937	. . . . . . . 8 |- ( Hom = Slot ( Hom ` ndx ) /\ ( Hom ` ndx ) e. NN )
263	262	simpri 113	. . . . . . 7 |- ( Hom ` ndx ) e. NN
264		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> H e. _V )
267		opexg 4262	. . . . . . 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 12940	. . . . . . . 8 |- (comp = Slot (comp ` ndx ) /\ (comp ` ndx ) e. NN )
270	269	simpri 113	. . . . . . 7 |- (comp ` ndx ) e. NN
271		mpoexga 6279	. . . . . . . . 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 2273	. . . . . . 7 |- ( ph -> .xb e. _V )
274		opexg 4262	. . . . . . 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 4245	. . . . . 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 4479	. . . . 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 4479	. . . 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 6054	. 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 2241	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 1364   T. wtru 1365   e. wcel 2167   A.wral 2475   _Vcvv 2763   [_csb 3084   u. cun 3155   C_ wss 3157   {csn 3623   {cpr 3624   {ctp 3625   <.cop 3626   U.cuni 3840   U_ciun 3917   class class class wbr 4034   {copab 4094   |-> cmpt 4095   X. cxp 4662   dom cdm 4664   ran crn 4665   o. ccom 4668   Fun wfun 5253   Fn wfn 5254   ` cfv 5259  (class class class)co 5925   e. cmpo 5927   1stc1st 6205   2ndc2nd 6206   ^m cmap 6716   X_cixp 6766   supcsup 7057   0cc0 7896   RR*cxr 8077   < clt 8078   NNcn 9007   ndxcnx 12700  Slot cslot 12702   Basecbs 12703   +g cplusg 12780   .rcmulr 12781  Scalarcsca 12783   .scvsca 12784   .icip 12785  TopSetcts 12786   lecple 12787   distcds 12789   Hom chom 12791  compcco 12792   TopOpenctopn 12942   Xt_cpt 12957   gsum_g cgsu 12959   X__scprds 12967

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4149  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-mulcom 7997  ax-addass 7998  ax-mulass 7999  ax-distr 8000  ax-i2m1 8001  ax-1rid 8003  ax-0id 8004  ax-rnegex 8005  ax-cnre 8007

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-tp 3631  df-op 3632  df-uni 3841  df-int 3876  df-iun 3919  df-br 4035  df-opab 4096  df-mpt 4097  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-res 4676  df-ima 4677  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-f1 5264  df-fo 5265  df-f1o 5266  df-fv 5267  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-1st 6207  df-2nd 6208  df-map 6718  df-ixp 6767  df-sup 7059  df-sub 8216  df-inn 9008  df-2 9066  df-3 9067  df-4 9068  df-5 9069  df-6 9070  df-7 9071  df-8 9072  df-9 9073  df-n0 9267  df-dec 9475  df-ndx 12706  df-slot 12707  df-base 12709  df-plusg 12793  df-mulr 12794  df-sca 12796  df-vsca 12797  df-ip 12798  df-tset 12799  df-ple 12800  df-ds 12802  df-hom 12804  df-cco 12805  df-rest 12943  df-topn 12944  df-topgen 12962  df-pt 12963  df-prds 12969

This theorem is referenced by:  prdsbaslemss  12976  prdssca  12977  prdsbas  12978  prdsplusg  12979  prdsmulr  12980