Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-prds Unicode version

Definition df-prds 13626
 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 usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.)
Assertion
Ref Expression
df-prds s Scalar TopSet comp comp
Distinct variable group:   ,,,,,,,,,,

Detailed syntax breakdown of Definition df-prds
StepHypRef Expression
1 cprds 13624 . 2 s
2 vs . . 3
3 vr . . 3
4 cvv 2916 . . 3
5 vv . . . 4
6 vx . . . . 5
73cv 1648 . . . . . 6
87cdm 4837 . . . . 5
96cv 1648 . . . . . . 7
109, 7cfv 5413 . . . . . 6
11 cbs 13424 . . . . . 6
1210, 11cfv 5413 . . . . 5
136, 8, 12cixp 7022 . . . 4
14 vh . . . . 5
15 vf . . . . . 6
16 vg . . . . . 6
175cv 1648 . . . . . 6
1815cv 1648 . . . . . . . . 9
199, 18cfv 5413 . . . . . . . 8
2016cv 1648 . . . . . . . . 9
219, 20cfv 5413 . . . . . . . 8
22 chom 13495 . . . . . . . . 9
2310, 22cfv 5413 . . . . . . . 8
2419, 21, 23co 6040 . . . . . . 7
256, 8, 24cixp 7022 . . . . . 6
2615, 16, 17, 17, 25cmpt2 6042 . . . . 5
27 cnx 13421 . . . . . . . . . 10
2827, 11cfv 5413 . . . . . . . . 9
2928, 17cop 3777 . . . . . . . 8
30 cplusg 13484 . . . . . . . . . 10
3127, 30cfv 5413 . . . . . . . . 9
3210, 30cfv 5413 . . . . . . . . . . . 12
3319, 21, 32co 6040 . . . . . . . . . . 11
346, 8, 33cmpt 4226 . . . . . . . . . 10
3515, 16, 17, 17, 34cmpt2 6042 . . . . . . . . 9
3631, 35cop 3777 . . . . . . . 8
37 cmulr 13485 . . . . . . . . . 10
3827, 37cfv 5413 . . . . . . . . 9
3910, 37cfv 5413 . . . . . . . . . . . 12
4019, 21, 39co 6040 . . . . . . . . . . 11
416, 8, 40cmpt 4226 . . . . . . . . . 10
4215, 16, 17, 17, 41cmpt2 6042 . . . . . . . . 9
4338, 42cop 3777 . . . . . . . 8
4429, 36, 43ctp 3776 . . . . . . 7
45 csca 13487 . . . . . . . . . 10 Scalar
4627, 45cfv 5413 . . . . . . . . 9 Scalar
472cv 1648 . . . . . . . . 9
4846, 47cop 3777 . . . . . . . 8 Scalar
49 cvsca 13488 . . . . . . . . . 10
5027, 49cfv 5413 . . . . . . . . 9
5147, 11cfv 5413 . . . . . . . . . 10
5210, 49cfv 5413 . . . . . . . . . . . 12
5318, 21, 52co 6040 . . . . . . . . . . 11
546, 8, 53cmpt 4226 . . . . . . . . . 10
5515, 16, 51, 17, 54cmpt2 6042 . . . . . . . . 9
5650, 55cop 3777 . . . . . . . 8
5748, 56cpr 3775 . . . . . . 7 Scalar
5844, 57cun 3278 . . . . . 6 Scalar
59 cts 13490 . . . . . . . . . 10 TopSet
6027, 59cfv 5413 . . . . . . . . 9 TopSet
61 ctopn 13604 . . . . . . . . . . 11
6261, 7ccom 4841 . . . . . . . . . 10
63 cpt 13621 . . . . . . . . . 10
6462, 63cfv 5413 . . . . . . . . 9
6560, 64cop 3777 . . . . . . . 8 TopSet
66 cple 13491 . . . . . . . . . 10
6727, 66cfv 5413 . . . . . . . . 9
6818, 20cpr 3775 . . . . . . . . . . . 12
6968, 17wss 3280 . . . . . . . . . . 11
7010, 66cfv 5413 . . . . . . . . . . . . 13
7119, 21, 70wbr 4172 . . . . . . . . . . . 12
7271, 6, 8wral 2666 . . . . . . . . . . 11
7369, 72wa 359 . . . . . . . . . 10
7473, 15, 16copab 4225 . . . . . . . . 9
7567, 74cop 3777 . . . . . . . 8
76 cds 13493 . . . . . . . . . 10
7727, 76cfv 5413 . . . . . . . . 9
7810, 76cfv 5413 . . . . . . . . . . . . . . 15
7919, 21, 78co 6040 . . . . . . . . . . . . . 14
806, 8, 79cmpt 4226 . . . . . . . . . . . . 13
8180crn 4838 . . . . . . . . . . . 12
82 cc0 8946 . . . . . . . . . . . . 13
8382csn 3774 . . . . . . . . . . . 12
8481, 83cun 3278 . . . . . . . . . . 11
85 cxr 9075 . . . . . . . . . . 11
86 clt 9076 . . . . . . . . . . 11
8784, 85, 86csup 7403 . . . . . . . . . 10
8815, 16, 17, 17, 87cmpt2 6042 . . . . . . . . 9
8977, 88cop 3777 . . . . . . . 8
9065, 75, 89ctp 3776 . . . . . . 7 TopSet
9127, 22cfv 5413 . . . . . . . . 9
9214cv 1648 . . . . . . . . 9
9391, 92cop 3777 . . . . . . . 8
94 cco 13496 . . . . . . . . . 10 comp
9527, 94cfv 5413 . . . . . . . . 9 comp
96 va . . . . . . . . . 10
97 vc . . . . . . . . . 10
9817, 17cxp 4835 . . . . . . . . . 10
99 vd . . . . . . . . . . 11
100 ve . . . . . . . . . . 11
10197cv 1648 . . . . . . . . . . . 12
10296cv 1648 . . . . . . . . . . . . 13
103 c2nd 6307 . . . . . . . . . . . . 13
104102, 103cfv 5413 . . . . . . . . . . . 12
105101, 104, 92co 6040 . . . . . . . . . . 11
106102, 92cfv 5413 . . . . . . . . . . 11
10799cv 1648 . . . . . . . . . . . . . 14
1089, 107cfv 5413 . . . . . . . . . . . . 13
109100cv 1648 . . . . . . . . . . . . . 14
1109, 109cfv 5413 . . . . . . . . . . . . 13
111 c1st 6306 . . . . . . . . . . . . . . . . 17
112102, 111cfv 5413 . . . . . . . . . . . . . . . 16
1139, 112cfv 5413 . . . . . . . . . . . . . . 15
1149, 104cfv 5413 . . . . . . . . . . . . . . 15
115113, 114cop 3777 . . . . . . . . . . . . . 14
1169, 101cfv 5413 . . . . . . . . . . . . . 14
11710, 94cfv 5413 . . . . . . . . . . . . . 14 comp
118115, 116, 117co 6040 . . . . . . . . . . . . 13 comp
119108, 110, 118co 6040 . . . . . . . . . . . 12 comp
1206, 8, 119cmpt 4226 . . . . . . . . . . 11 comp
12199, 100, 105, 106, 120cmpt2 6042 . . . . . . . . . 10 comp
12296, 97, 98, 17, 121cmpt2 6042 . . . . . . . . 9 comp
12395, 122cop 3777 . . . . . . . 8 comp comp
12493, 123cpr 3775 . . . . . . 7 comp comp
12590, 124cun 3278 . . . . . 6 TopSet comp comp
12658, 125cun 3278 . . . . 5 Scalar TopSet comp comp
12714, 26, 126csb 3211 . . . 4 Scalar TopSet comp comp
1285, 13, 127csb 3211 . . 3 Scalar TopSet comp comp
1292, 3, 4, 4, 128cmpt2 6042 . 2 Scalar TopSet comp comp
1301, 129wceq 1649 1 s Scalar TopSet comp comp
 Colors of variables: wff set class This definition is referenced by:  reldmprds  13627  prdsval  13633
 Copyright terms: Public domain W3C validator