Definition df-prds 12721

Description: Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)

Assertion

Ref

Expression

df-prds

|- 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. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )

Distinct variable group:   a, c, d, e, f, g, h, s, r, x, v

Detailed syntax breakdown of Definition df-prds

Step	Hyp	Ref	Expression
1		cprds 12719	. 2 class X_s
2		vs	. . 3 setvar s
3		vr	. . 3 setvar r
4		cvv 2739	. . 3 class _V
5		vv	. . . 4 setvar v
6		vx	. . . . 5 setvar x
7	3	cv 1352	. . . . . 6 class r
8	7	cdm 4628	. . . . 5 class dom r
9	6	cv 1352	. . . . . . 7 class x
10	9, 7	cfv 5218	. . . . . 6 class ( r ` x )
11		cbs 12464	. . . . . 6 class Base
12	10, 11	cfv 5218	. . . . 5 class ( Base ` ( r ` x ) )
13	6, 8, 12	cixp 6700	. . . 4 class X_ x e. dom r ( Base ` ( r ` x ) )
14		vh	. . . . 5 setvar h
15		vf	. . . . . 6 setvar f
16		vg	. . . . . 6 setvar g
17	5	cv 1352	. . . . . 6 class v
18	15	cv 1352	. . . . . . . . 9 class f
19	9, 18	cfv 5218	. . . . . . . 8 class ( f ` x )
20	16	cv 1352	. . . . . . . . 9 class g
21	9, 20	cfv 5218	. . . . . . . 8 class ( g ` x )
22		chom 12549	. . . . . . . . 9 class Hom
23	10, 22	cfv 5218	. . . . . . . 8 class ( Hom ` ( r ` x ) )
24	19, 21, 23	co 5877	. . . . . . 7 class ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) )
25	6, 8, 24	cixp 6700	. . . . . 6 class X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) )
26	15, 16, 17, 17, 25	cmpo 5879	. . . . 5 class ( f e. v , g e. v |-> X_ x e. dom r ( ( f ` x ) ( Hom ` ( r ` x ) ) ( g ` x ) ) )
27		cnx 12461	. . . . . . . . . 10 class ndx
28	27, 11	cfv 5218	. . . . . . . . 9 class ( Base ` ndx )
29	28, 17	cop 3597	. . . . . . . 8 class <. ( Base ` ndx ) , v >.
30		cplusg 12538	. . . . . . . . . 10 class +g
31	27, 30	cfv 5218	. . . . . . . . 9 class ( +g ` ndx )
32	10, 30	cfv 5218	. . . . . . . . . . . 12 class ( +g ` ( r ` x ) )
33	19, 21, 32	co 5877	. . . . . . . . . . 11 class ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) )
34	6, 8, 33	cmpt 4066	. . . . . . . . . 10 class ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) )
35	15, 16, 17, 17, 34	cmpo 5879	. . . . . . . . 9 class ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) )
36	31, 35	cop 3597	. . . . . . . 8 class <. ( +g ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( +g ` ( r ` x ) ) ( g ` x ) ) ) ) >.
37		cmulr 12539	. . . . . . . . . 10 class .r
38	27, 37	cfv 5218	. . . . . . . . 9 class ( .r ` ndx )
39	10, 37	cfv 5218	. . . . . . . . . . . 12 class ( .r ` ( r ` x ) )
40	19, 21, 39	co 5877	. . . . . . . . . . 11 class ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) )
41	6, 8, 40	cmpt 4066	. . . . . . . . . 10 class ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) )
42	15, 16, 17, 17, 41	cmpo 5879	. . . . . . . . 9 class ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) )
43	38, 42	cop 3597	. . . . . . . 8 class <. ( .r ` ndx ) , ( f e. v , g e. v |-> ( x e. dom r |-> ( ( f ` x ) ( .r ` ( r ` x ) ) ( g ` x ) ) ) ) >.
44	29, 36, 43	ctp 3596	. . . . . . 7 class { <. ( 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 ) ) ) ) >. }
45		csca 12541	. . . . . . . . . 10 class Scalar
46	27, 45	cfv 5218	. . . . . . . . 9 class (Scalar ` ndx )
47	2	cv 1352	. . . . . . . . 9 class s
48	46, 47	cop 3597	. . . . . . . 8 class <. (Scalar ` ndx ) , s >.
49		cvsca 12542	. . . . . . . . . 10 class .s
50	27, 49	cfv 5218	. . . . . . . . 9 class ( .s ` ndx )
51	47, 11	cfv 5218	. . . . . . . . . 10 class ( Base ` s )
52	10, 49	cfv 5218	. . . . . . . . . . . 12 class ( .s ` ( r ` x ) )
53	18, 21, 52	co 5877	. . . . . . . . . . 11 class ( f ( .s ` ( r ` x ) ) ( g ` x ) )
54	6, 8, 53	cmpt 4066	. . . . . . . . . 10 class ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) )
55	15, 16, 51, 17, 54	cmpo 5879	. . . . . . . . 9 class ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) )
56	50, 55	cop 3597	. . . . . . . 8 class <. ( .s ` ndx ) , ( f e. ( Base ` s ) , g e. v |-> ( x e. dom r |-> ( f ( .s ` ( r ` x ) ) ( g ` x ) ) ) ) >.
57		cip 12543	. . . . . . . . . 10 class .i
58	27, 57	cfv 5218	. . . . . . . . 9 class ( .i ` ndx )
59	10, 57	cfv 5218	. . . . . . . . . . . . 13 class ( .i ` ( r ` x ) )
60	19, 21, 59	co 5877	. . . . . . . . . . . 12 class ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) )
61	6, 8, 60	cmpt 4066	. . . . . . . . . . 11 class ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) )
62		cgsu 12711	. . . . . . . . . . 11 class gsumg
63	47, 61, 62	co 5877	. . . . . . . . . 10 class ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) )
64	15, 16, 17, 17, 63	cmpo 5879	. . . . . . . . 9 class ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) )
65	58, 64	cop 3597	. . . . . . . 8 class <. ( .i ` ndx ) , ( f e. v , g e. v |-> ( s gsumg ( x e. dom r |-> ( ( f ` x ) ( .i ` ( r ` x ) ) ( g ` x ) ) ) ) ) >.
66	48, 56, 65	ctp 3596	. . . . . . 7 class { <. (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 ) ) ) ) ) >. }
67	44, 66	cun 3129	. . . . . 6 class ( { <. ( 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 ) ) ) ) ) >. } )
68		cts 12544	. . . . . . . . . 10 class TopSet
69	27, 68	cfv 5218	. . . . . . . . 9 class (TopSet ` ndx )
70		ctopn 12694	. . . . . . . . . . 11 class TopOpen
71	70, 7	ccom 4632	. . . . . . . . . 10 class ( TopOpen o. r )
72		cpt 12709	. . . . . . . . . 10 class Xt_
73	71, 72	cfv 5218	. . . . . . . . 9 class ( Xt_ ` ( TopOpen o. r ) )
74	69, 73	cop 3597	. . . . . . . 8 class <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >.
75		cple 12545	. . . . . . . . . 10 class le
76	27, 75	cfv 5218	. . . . . . . . 9 class ( le ` ndx )
77	18, 20	cpr 3595	. . . . . . . . . . . 12 class { f , g }
78	77, 17	wss 3131	. . . . . . . . . . 11 wff { f , g } C_ v
79	10, 75	cfv 5218	. . . . . . . . . . . . 13 class ( le ` ( r ` x ) )
80	19, 21, 79	wbr 4005	. . . . . . . . . . . 12 wff ( f ` x ) ( le ` ( r ` x ) ) ( g ` x )
81	80, 6, 8	wral 2455	. . . . . . . . . . 11 wff A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x )
82	78, 81	wa 104	. . . . . . . . . 10 wff ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) )
83	82, 15, 16	copab 4065	. . . . . . . . 9 class { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) }
84	76, 83	cop 3597	. . . . . . . 8 class <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >.
85		cds 12547	. . . . . . . . . 10 class dist
86	27, 85	cfv 5218	. . . . . . . . 9 class ( dist ` ndx )
87	10, 85	cfv 5218	. . . . . . . . . . . . . . 15 class ( dist ` ( r ` x ) )
88	19, 21, 87	co 5877	. . . . . . . . . . . . . 14 class ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) )
89	6, 8, 88	cmpt 4066	. . . . . . . . . . . . 13 class ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) )
90	89	crn 4629	. . . . . . . . . . . 12 class ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) )
91		cc0 7813	. . . . . . . . . . . . 13 class 0
92	91	csn 3594	. . . . . . . . . . . 12 class { 0 }
93	90, 92	cun 3129	. . . . . . . . . . 11 class ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } )
94		cxr 7993	. . . . . . . . . . 11 class RR*
95		clt 7994	. . . . . . . . . . 11 class <
96	93, 94, 95	csup 6983	. . . . . . . . . 10 class sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < )
97	15, 16, 17, 17, 96	cmpo 5879	. . . . . . . . 9 class ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) )
98	86, 97	cop 3597	. . . . . . . 8 class <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >.
99	74, 84, 98	ctp 3596	. . . . . . 7 class { <. (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* , < ) ) >. }
100	27, 22	cfv 5218	. . . . . . . . 9 class ( Hom ` ndx )
101	14	cv 1352	. . . . . . . . 9 class h
102	100, 101	cop 3597	. . . . . . . 8 class <. ( Hom ` ndx ) , h >.
103		cco 12550	. . . . . . . . . 10 class comp
104	27, 103	cfv 5218	. . . . . . . . 9 class (comp ` ndx )
105		va	. . . . . . . . . 10 setvar a
106		vc	. . . . . . . . . 10 setvar c
107	17, 17	cxp 4626	. . . . . . . . . 10 class ( v X. v )
108		vd	. . . . . . . . . . 11 setvar d
109		ve	. . . . . . . . . . 11 setvar e
110	106	cv 1352	. . . . . . . . . . . 12 class c
111	105	cv 1352	. . . . . . . . . . . . 13 class a
112		c2nd 6142	. . . . . . . . . . . . 13 class 2nd
113	111, 112	cfv 5218	. . . . . . . . . . . 12 class ( 2nd ` a )
114	110, 113, 101	co 5877	. . . . . . . . . . 11 class ( c h ( 2nd ` a ) )
115	111, 101	cfv 5218	. . . . . . . . . . 11 class ( h ` a )
116	108	cv 1352	. . . . . . . . . . . . . 14 class d
117	9, 116	cfv 5218	. . . . . . . . . . . . 13 class ( d ` x )
118	109	cv 1352	. . . . . . . . . . . . . 14 class e
119	9, 118	cfv 5218	. . . . . . . . . . . . 13 class ( e ` x )
120		c1st 6141	. . . . . . . . . . . . . . . . 17 class 1st
121	111, 120	cfv 5218	. . . . . . . . . . . . . . . 16 class ( 1st ` a )
122	9, 121	cfv 5218	. . . . . . . . . . . . . . 15 class ( ( 1st ` a ) ` x )
123	9, 113	cfv 5218	. . . . . . . . . . . . . . 15 class ( ( 2nd ` a ) ` x )
124	122, 123	cop 3597	. . . . . . . . . . . . . 14 class <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >.
125	9, 110	cfv 5218	. . . . . . . . . . . . . 14 class ( c ` x )
126	10, 103	cfv 5218	. . . . . . . . . . . . . 14 class (comp ` ( r ` x ) )
127	124, 125, 126	co 5877	. . . . . . . . . . . . 13 class ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) )
128	117, 119, 127	co 5877	. . . . . . . . . . . 12 class ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) )
129	6, 8, 128	cmpt 4066	. . . . . . . . . . 11 class ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) )
130	108, 109, 114, 115, 129	cmpo 5879	. . . . . . . . . 10 class ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) )
131	105, 106, 107, 17, 130	cmpo 5879	. . . . . . . . 9 class ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) )
132	104, 131	cop 3597	. . . . . . . 8 class <. (comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >.
133	102, 132	cpr 3595	. . . . . . 7 class { <. ( Hom ` ndx ) , h >. , <. (comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. }
134	99, 133	cun 3129	. . . . . 6 class ( { <. (TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. r ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ v /\ A. x e. dom r ( f ` x ) ( le ` ( r ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. v , g e. v |-> sup ( ( ran ( x e. dom r |-> ( ( f ` x ) ( dist ` ( r ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , h >. , <. (comp ` ndx ) , ( a e. ( v X. v ) , c e. v |-> ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } )
135	67, 134	cun 3129	. . . . 5 class ( ( { <. ( 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. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
136	14, 26, 135	csb 3059	. . . 4 class [_ ( 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. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
137	5, 13, 136	csb 3059	. . 3 class [_ 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. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
138	2, 3, 4, 4, 137	cmpo 5879	. 2 class ( 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. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
139	1, 138	wceq 1353	1 wff 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. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. (comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )

This definition is referenced by:  reldmprds  12722  prdsex  12723