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

Definition df-prds 13676
 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 13674 . 2 s
2 vs . . 3
3 vr . . 3
4 cvv 2958 . . 3
5 vv . . . 4
6 vx . . . . 5
73cv 1652 . . . . . 6
87cdm 4881 . . . . 5
96cv 1652 . . . . . . 7
109, 7cfv 5457 . . . . . 6
11 cbs 13474 . . . . . 6
1210, 11cfv 5457 . . . . 5
136, 8, 12cixp 7066 . . . 4
14 vh . . . . 5
15 vf . . . . . 6
16 vg . . . . . 6
175cv 1652 . . . . . 6
1815cv 1652 . . . . . . . . 9
199, 18cfv 5457 . . . . . . . 8
2016cv 1652 . . . . . . . . 9
219, 20cfv 5457 . . . . . . . 8
22 chom 13545 . . . . . . . . 9
2310, 22cfv 5457 . . . . . . . 8
2419, 21, 23co 6084 . . . . . . 7
256, 8, 24cixp 7066 . . . . . 6
2615, 16, 17, 17, 25cmpt2 6086 . . . . 5
27 cnx 13471 . . . . . . . . . 10
2827, 11cfv 5457 . . . . . . . . 9
2928, 17cop 3819 . . . . . . . 8
30 cplusg 13534 . . . . . . . . . 10
3127, 30cfv 5457 . . . . . . . . 9
3210, 30cfv 5457 . . . . . . . . . . . 12
3319, 21, 32co 6084 . . . . . . . . . . 11
346, 8, 33cmpt 4269 . . . . . . . . . 10
3515, 16, 17, 17, 34cmpt2 6086 . . . . . . . . 9
3631, 35cop 3819 . . . . . . . 8
37 cmulr 13535 . . . . . . . . . 10
3827, 37cfv 5457 . . . . . . . . 9
3910, 37cfv 5457 . . . . . . . . . . . 12
4019, 21, 39co 6084 . . . . . . . . . . 11
416, 8, 40cmpt 4269 . . . . . . . . . 10
4215, 16, 17, 17, 41cmpt2 6086 . . . . . . . . 9
4338, 42cop 3819 . . . . . . . 8
4429, 36, 43ctp 3818 . . . . . . 7
45 csca 13537 . . . . . . . . . 10 Scalar
4627, 45cfv 5457 . . . . . . . . 9 Scalar
472cv 1652 . . . . . . . . 9
4846, 47cop 3819 . . . . . . . 8 Scalar
49 cvsca 13538 . . . . . . . . . 10
5027, 49cfv 5457 . . . . . . . . 9
5147, 11cfv 5457 . . . . . . . . . 10
5210, 49cfv 5457 . . . . . . . . . . . 12
5318, 21, 52co 6084 . . . . . . . . . . 11
546, 8, 53cmpt 4269 . . . . . . . . . 10
5515, 16, 51, 17, 54cmpt2 6086 . . . . . . . . 9
5650, 55cop 3819 . . . . . . . 8
5748, 56cpr 3817 . . . . . . 7 Scalar
5844, 57cun 3320 . . . . . 6 Scalar
59 cts 13540 . . . . . . . . . 10 TopSet
6027, 59cfv 5457 . . . . . . . . 9 TopSet
61 ctopn 13654 . . . . . . . . . . 11
6261, 7ccom 4885 . . . . . . . . . 10
63 cpt 13671 . . . . . . . . . 10
6462, 63cfv 5457 . . . . . . . . 9
6560, 64cop 3819 . . . . . . . 8 TopSet
66 cple 13541 . . . . . . . . . 10
6727, 66cfv 5457 . . . . . . . . 9
6818, 20cpr 3817 . . . . . . . . . . . 12
6968, 17wss 3322 . . . . . . . . . . 11
7010, 66cfv 5457 . . . . . . . . . . . . 13
7119, 21, 70wbr 4215 . . . . . . . . . . . 12
7271, 6, 8wral 2707 . . . . . . . . . . 11
7369, 72wa 360 . . . . . . . . . 10
7473, 15, 16copab 4268 . . . . . . . . 9
7567, 74cop 3819 . . . . . . . 8
76 cds 13543 . . . . . . . . . 10
7727, 76cfv 5457 . . . . . . . . 9
7810, 76cfv 5457 . . . . . . . . . . . . . . 15
7919, 21, 78co 6084 . . . . . . . . . . . . . 14
806, 8, 79cmpt 4269 . . . . . . . . . . . . 13
8180crn 4882 . . . . . . . . . . . 12
82 cc0 8995 . . . . . . . . . . . . 13
8382csn 3816 . . . . . . . . . . . 12
8481, 83cun 3320 . . . . . . . . . . 11
85 cxr 9124 . . . . . . . . . . 11
86 clt 9125 . . . . . . . . . . 11
8784, 85, 86csup 7448 . . . . . . . . . 10
8815, 16, 17, 17, 87cmpt2 6086 . . . . . . . . 9
8977, 88cop 3819 . . . . . . . 8
9065, 75, 89ctp 3818 . . . . . . 7 TopSet
9127, 22cfv 5457 . . . . . . . . 9
9214cv 1652 . . . . . . . . 9
9391, 92cop 3819 . . . . . . . 8
94 cco 13546 . . . . . . . . . 10 comp
9527, 94cfv 5457 . . . . . . . . 9 comp
96 va . . . . . . . . . 10
97 vc . . . . . . . . . 10
9817, 17cxp 4879 . . . . . . . . . 10
99 vd . . . . . . . . . . 11
100 ve . . . . . . . . . . 11
10197cv 1652 . . . . . . . . . . . 12
10296cv 1652 . . . . . . . . . . . . 13
103 c2nd 6351 . . . . . . . . . . . . 13
104102, 103cfv 5457 . . . . . . . . . . . 12
105101, 104, 92co 6084 . . . . . . . . . . 11
106102, 92cfv 5457 . . . . . . . . . . 11
10799cv 1652 . . . . . . . . . . . . . 14
1089, 107cfv 5457 . . . . . . . . . . . . 13
109100cv 1652 . . . . . . . . . . . . . 14
1109, 109cfv 5457 . . . . . . . . . . . . 13
111 c1st 6350 . . . . . . . . . . . . . . . . 17
112102, 111cfv 5457 . . . . . . . . . . . . . . . 16
1139, 112cfv 5457 . . . . . . . . . . . . . . 15
1149, 104cfv 5457 . . . . . . . . . . . . . . 15
115113, 114cop 3819 . . . . . . . . . . . . . 14
1169, 101cfv 5457 . . . . . . . . . . . . . 14
11710, 94cfv 5457 . . . . . . . . . . . . . 14 comp
118115, 116, 117co 6084 . . . . . . . . . . . . 13 comp
119108, 110, 118co 6084 . . . . . . . . . . . 12 comp
1206, 8, 119cmpt 4269 . . . . . . . . . . 11 comp
12199, 100, 105, 106, 120cmpt2 6086 . . . . . . . . . 10 comp
12296, 97, 98, 17, 121cmpt2 6086 . . . . . . . . 9 comp
12395, 122cop 3819 . . . . . . . 8 comp comp
12493, 123cpr 3817 . . . . . . 7 comp comp
12590, 124cun 3320 . . . . . 6 TopSet comp comp
12658, 125cun 3320 . . . . 5 Scalar TopSet comp comp
12714, 26, 126csb 3253 . . . 4 Scalar TopSet comp comp
1285, 13, 127csb 3253 . . 3 Scalar TopSet comp comp
1292, 3, 4, 4, 128cmpt2 6086 . 2 Scalar TopSet comp comp
1301, 129wceq 1653 1 s Scalar TopSet comp comp
 Colors of variables: wff set class This definition is referenced by:  reldmprds  13677  prdsval  13683
 Copyright terms: Public domain W3C validator