Metamath Proof Explorer


Definition df-prds

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

Ref Expression
Assertion df-prds 𝑠 = s V , r V x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprds class 𝑠
1 vs setvar s
2 cvv class V
3 vr setvar r
4 vx setvar x
5 3 cv setvar r
6 5 cdm class dom r
7 cbs class Base
8 4 cv setvar x
9 8 5 cfv class r x
10 9 7 cfv class Base r x
11 4 6 10 cixp class x dom r Base r x
12 vv setvar v
13 vf setvar f
14 12 cv setvar v
15 vg setvar g
16 13 cv setvar f
17 8 16 cfv class f x
18 chom class Hom
19 9 18 cfv class Hom r x
20 15 cv setvar g
21 8 20 cfv class g x
22 17 21 19 co class f x Hom r x g x
23 4 6 22 cixp class x dom r f x Hom r x g x
24 13 15 14 14 23 cmpo class f v , g v x dom r f x Hom r x g x
25 vh setvar h
26 cnx class ndx
27 26 7 cfv class Base ndx
28 27 14 cop class Base ndx v
29 cplusg class + 𝑔
30 26 29 cfv class + ndx
31 9 29 cfv class + r x
32 17 21 31 co class f x + r x g x
33 4 6 32 cmpt class x dom r f x + r x g x
34 13 15 14 14 33 cmpo class f v , g v x dom r f x + r x g x
35 30 34 cop class + ndx f v , g v x dom r f x + r x g x
36 cmulr class 𝑟
37 26 36 cfv class ndx
38 9 36 cfv class r x
39 17 21 38 co class f x r x g x
40 4 6 39 cmpt class x dom r f x r x g x
41 13 15 14 14 40 cmpo class f v , g v x dom r f x r x g x
42 37 41 cop class ndx f v , g v x dom r f x r x g x
43 28 35 42 ctp class Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x
44 csca class Scalar
45 26 44 cfv class Scalar ndx
46 1 cv setvar s
47 45 46 cop class Scalar ndx s
48 cvsca class 𝑠
49 26 48 cfv class ndx
50 46 7 cfv class Base s
51 9 48 cfv class r x
52 16 21 51 co class f r x g x
53 4 6 52 cmpt class x dom r f r x g x
54 13 15 50 14 53 cmpo class f Base s , g v x dom r f r x g x
55 49 54 cop class ndx f Base s , g v x dom r f r x g x
56 cip class 𝑖
57 26 56 cfv class 𝑖 ndx
58 cgsu class Σ𝑔
59 9 56 cfv class 𝑖 r x
60 17 21 59 co class f x 𝑖 r x g x
61 4 6 60 cmpt class x dom r f x 𝑖 r x g x
62 46 61 58 co class s x dom r f x 𝑖 r x g x
63 13 15 14 14 62 cmpo class f v , g v s x dom r f x 𝑖 r x g x
64 57 63 cop class 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x
65 47 55 64 ctp class Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x
66 43 65 cun class Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x
67 cts class TopSet
68 26 67 cfv class TopSet ndx
69 cpt class 𝑡
70 ctopn class TopOpen
71 70 5 ccom class TopOpen r
72 71 69 cfv class 𝑡 TopOpen r
73 68 72 cop class TopSet ndx 𝑡 TopOpen r
74 cple class le
75 26 74 cfv class ndx
76 16 20 cpr class f g
77 76 14 wss wff f g v
78 9 74 cfv class r x
79 17 21 78 wbr wff f x r x g x
80 79 4 6 wral wff x dom r f x r x g x
81 77 80 wa wff f g v x dom r f x r x g x
82 81 13 15 copab class f g | f g v x dom r f x r x g x
83 75 82 cop class ndx f g | f g v x dom r f x r x g x
84 cds class dist
85 26 84 cfv class dist ndx
86 9 84 cfv class dist r x
87 17 21 86 co class f x dist r x g x
88 4 6 87 cmpt class x dom r f x dist r x g x
89 88 crn class ran x dom r f x dist r x g x
90 cc0 class 0
91 90 csn class 0
92 89 91 cun class ran x dom r f x dist r x g x 0
93 cxr class *
94 clt class <
95 92 93 94 csup class sup ran x dom r f x dist r x g x 0 * <
96 13 15 14 14 95 cmpo class f v , g v sup ran x dom r f x dist r x g x 0 * <
97 85 96 cop class dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * <
98 73 83 97 ctp class TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * <
99 26 18 cfv class Hom ndx
100 25 cv setvar h
101 99 100 cop class Hom ndx h
102 cco class comp
103 26 102 cfv class comp ndx
104 va setvar a
105 14 14 cxp class v × v
106 vc setvar c
107 vd setvar d
108 c2nd class 2 nd
109 104 cv setvar a
110 109 108 cfv class 2 nd a
111 106 cv setvar c
112 110 111 100 co class 2 nd a h c
113 ve setvar e
114 109 100 cfv class h a
115 107 cv setvar d
116 8 115 cfv class d x
117 c1st class 1 st
118 109 117 cfv class 1 st a
119 8 118 cfv class 1 st a x
120 8 110 cfv class 2 nd a x
121 119 120 cop class 1 st a x 2 nd a x
122 9 102 cfv class comp r x
123 8 111 cfv class c x
124 121 123 122 co class 1 st a x 2 nd a x comp r x c x
125 113 cv setvar e
126 8 125 cfv class e x
127 116 126 124 co class d x 1 st a x 2 nd a x comp r x c x e x
128 4 6 127 cmpt class x dom r d x 1 st a x 2 nd a x comp r x c x e x
129 107 113 112 114 128 cmpo class d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
130 104 106 105 14 129 cmpo class a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
131 103 130 cop class comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
132 101 131 cpr class Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
133 98 132 cun class TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
134 66 133 cun class Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
135 25 24 134 csb class f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
136 12 11 135 csb class x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
137 1 3 2 2 136 cmpo class s V , r V x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x
138 0 137 wceq wff 𝑠 = s V , r V x dom r Base r x / v f v , g v x dom r f x Hom r x g x / h Base ndx v + ndx f v , g v x dom r f x + r x g x ndx f v , g v x dom r f x r x g x Scalar ndx s ndx f Base s , g v x dom r f r x g x 𝑖 ndx f v , g v s x dom r f x 𝑖 r x g x TopSet ndx 𝑡 TopOpen r ndx f g | f g v x dom r f x r x g x dist ndx f v , g v sup ran x dom r f x dist r x g x 0 * < Hom ndx h comp ndx a v × v , c v d 2 nd a h c , e h a x dom r d x 1 st a x 2 nd a x comp r x c x e x