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

Definition df-imas 14762
 Description: Define an image structure, which takes a structure and a function on the base set, and maps all the operations via the function. For this to work properly must either be injective or satisfy the well-definedness condition for each relevant operation. Note that although we call this an "image" by association to df-ima 5012, in order to keep the definition simple we consider only the case when the domain of is equal to the base set of . Other cases can be achieved by restricting (with df-res 5011) and/or ( with df-ress 14496) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.)
Assertion
Ref Expression
df-imas s Scalar Scalar Scalar TopSet qTop g
Distinct variable group:   ,,,,,,,,,,

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 14758 . 2 s
2 vf . . 3
3 vr . . 3
4 cvv 3113 . . 3
5 vv . . . 4
63cv 1378 . . . . 5
7 cbs 14489 . . . . 5
86, 7cfv 5587 . . . 4
9 cnx 14486 . . . . . . . . 9
109, 7cfv 5587 . . . . . . . 8
112cv 1378 . . . . . . . . 9
1211crn 5000 . . . . . . . 8
1310, 12cop 4033 . . . . . . 7
14 cplusg 14554 . . . . . . . . 9
159, 14cfv 5587 . . . . . . . 8
16 vp . . . . . . . . 9
175cv 1378 . . . . . . . . 9
18 vq . . . . . . . . . 10
1916cv 1378 . . . . . . . . . . . . . 14
2019, 11cfv 5587 . . . . . . . . . . . . 13
2118cv 1378 . . . . . . . . . . . . . 14
2221, 11cfv 5587 . . . . . . . . . . . . 13
2320, 22cop 4033 . . . . . . . . . . . 12
246, 14cfv 5587 . . . . . . . . . . . . . 14
2519, 21, 24co 6283 . . . . . . . . . . . . 13
2625, 11cfv 5587 . . . . . . . . . . . 12
2723, 26cop 4033 . . . . . . . . . . 11
2827csn 4027 . . . . . . . . . 10
2918, 17, 28ciun 4325 . . . . . . . . 9
3016, 17, 29ciun 4325 . . . . . . . 8
3115, 30cop 4033 . . . . . . 7
32 cmulr 14555 . . . . . . . . 9
339, 32cfv 5587 . . . . . . . 8
346, 32cfv 5587 . . . . . . . . . . . . . 14
3519, 21, 34co 6283 . . . . . . . . . . . . 13
3635, 11cfv 5587 . . . . . . . . . . . 12
3723, 36cop 4033 . . . . . . . . . . 11
3837csn 4027 . . . . . . . . . 10
3918, 17, 38ciun 4325 . . . . . . . . 9
4016, 17, 39ciun 4325 . . . . . . . 8
4133, 40cop 4033 . . . . . . 7
4213, 31, 41ctp 4031 . . . . . 6
43 csca 14557 . . . . . . . . 9 Scalar
449, 43cfv 5587 . . . . . . . 8 Scalar
456, 43cfv 5587 . . . . . . . 8 Scalar
4644, 45cop 4033 . . . . . . 7 Scalar Scalar
47 cvsca 14558 . . . . . . . . 9
489, 47cfv 5587 . . . . . . . 8
49 vx . . . . . . . . . 10
5045, 7cfv 5587 . . . . . . . . . 10 Scalar
5122csn 4027 . . . . . . . . . 10
526, 47cfv 5587 . . . . . . . . . . . 12
5319, 21, 52co 6283 . . . . . . . . . . 11
5453, 11cfv 5587 . . . . . . . . . 10
5516, 49, 50, 51, 54cmpt2 6285 . . . . . . . . 9 Scalar
5618, 17, 55ciun 4325 . . . . . . . 8 Scalar
5748, 56cop 4033 . . . . . . 7 Scalar
58 cip 14559 . . . . . . . . 9
599, 58cfv 5587 . . . . . . . 8
606, 58cfv 5587 . . . . . . . . . . . . 13
6119, 21, 60co 6283 . . . . . . . . . . . 12
6223, 61cop 4033 . . . . . . . . . . 11
6362csn 4027 . . . . . . . . . 10
6418, 17, 63ciun 4325 . . . . . . . . 9
6516, 17, 64ciun 4325 . . . . . . . 8
6659, 65cop 4033 . . . . . . 7
6746, 57, 66ctp 4031 . . . . . 6 Scalar Scalar Scalar
6842, 67cun 3474 . . . . 5 Scalar Scalar Scalar
69 cts 14560 . . . . . . . 8 TopSet
709, 69cfv 5587 . . . . . . 7 TopSet
71 ctopn 14676 . . . . . . . . 9
726, 71cfv 5587 . . . . . . . 8
73 cqtop 14757 . . . . . . . 8 qTop
7472, 11, 73co 6283 . . . . . . 7 qTop
7570, 74cop 4033 . . . . . 6 TopSet qTop
76 cple 14561 . . . . . . . 8
779, 76cfv 5587 . . . . . . 7
786, 76cfv 5587 . . . . . . . . 9
7911, 78ccom 5003 . . . . . . . 8
8011ccnv 4998 . . . . . . . 8
8179, 80ccom 5003 . . . . . . 7
8277, 81cop 4033 . . . . . 6
83 cds 14563 . . . . . . . 8
849, 83cfv 5587 . . . . . . 7
85 vy . . . . . . . 8
86 vn . . . . . . . . . 10
87 cn 10535 . . . . . . . . . 10
88 vg . . . . . . . . . . . 12
89 c1 9492 . . . . . . . . . . . . . . . . . 18
90 vh . . . . . . . . . . . . . . . . . . 19
9190cv 1378 . . . . . . . . . . . . . . . . . 18
9289, 91cfv 5587 . . . . . . . . . . . . . . . . 17
93 c1st 6782 . . . . . . . . . . . . . . . . 17
9492, 93cfv 5587 . . . . . . . . . . . . . . . 16
9594, 11cfv 5587 . . . . . . . . . . . . . . 15
9649cv 1378 . . . . . . . . . . . . . . 15
9795, 96wceq 1379 . . . . . . . . . . . . . 14
9886cv 1378 . . . . . . . . . . . . . . . . . 18
9998, 91cfv 5587 . . . . . . . . . . . . . . . . 17
100 c2nd 6783 . . . . . . . . . . . . . . . . 17
10199, 100cfv 5587 . . . . . . . . . . . . . . . 16
102101, 11cfv 5587 . . . . . . . . . . . . . . 15
10385cv 1378 . . . . . . . . . . . . . . 15
104102, 103wceq 1379 . . . . . . . . . . . . . 14
105 vi . . . . . . . . . . . . . . . . . . . 20
106105cv 1378 . . . . . . . . . . . . . . . . . . 19
107106, 91cfv 5587 . . . . . . . . . . . . . . . . . 18
108107, 100cfv 5587 . . . . . . . . . . . . . . . . 17
109108, 11cfv 5587 . . . . . . . . . . . . . . . 16
110 caddc 9494 . . . . . . . . . . . . . . . . . . . 20
111106, 89, 110co 6283 . . . . . . . . . . . . . . . . . . 19
112111, 91cfv 5587 . . . . . . . . . . . . . . . . . 18
113112, 93cfv 5587 . . . . . . . . . . . . . . . . 17
114113, 11cfv 5587 . . . . . . . . . . . . . . . 16
115109, 114wceq 1379 . . . . . . . . . . . . . . 15
116 cmin 9804 . . . . . . . . . . . . . . . . 17
11798, 89, 116co 6283 . . . . . . . . . . . . . . . 16
118 cfz 11671 . . . . . . . . . . . . . . . 16
11989, 117, 118co 6283 . . . . . . . . . . . . . . 15
120115, 105, 119wral 2814 . . . . . . . . . . . . . 14
12197, 104, 120w3a 973 . . . . . . . . . . . . 13
12217, 17cxp 4997 . . . . . . . . . . . . . 14
12389, 98, 118co 6283 . . . . . . . . . . . . . 14
124 cmap 7420 . . . . . . . . . . . . . 14
125122, 123, 124co 6283 . . . . . . . . . . . . 13
126121, 90, 125crab 2818 . . . . . . . . . . . 12
127 cxrs 14754 . . . . . . . . . . . . 13
1286, 83cfv 5587 . . . . . . . . . . . . . 14
12988cv 1378 . . . . . . . . . . . . . 14
130128, 129ccom 5003 . . . . . . . . . . . . 13
131 cgsu 14695 . . . . . . . . . . . . 13 g
132127, 130, 131co 6283 . . . . . . . . . . . 12 g
13388, 126, 132cmpt 4505 . . . . . . . . . . 11 g
134133crn 5000 . . . . . . . . . 10 g
13586, 87, 134ciun 4325 . . . . . . . . 9 g
136 cxr 9626 . . . . . . . . 9
137 clt 9627 . . . . . . . . . 10
138137ccnv 4998 . . . . . . . . 9
139135, 136, 138csup 7899 . . . . . . . 8 g
14049, 85, 12, 12, 139cmpt2 6285 . . . . . . 7 g
14184, 140cop 4033 . . . . . 6 g
14275, 82, 141ctp 4031 . . . . 5 TopSet qTop g
14368, 142cun 3474 . . . 4 Scalar Scalar Scalar TopSet qTop g
1445, 8, 143csb 3435 . . 3 Scalar Scalar Scalar TopSet qTop g
1452, 3, 4, 4, 144cmpt2 6285 . 2 Scalar Scalar Scalar TopSet qTop g
1461, 145wceq 1379 1 s Scalar Scalar Scalar TopSet qTop g
 Colors of variables: wff setvar class This definition is referenced by:  imasval  14765
 Copyright terms: Public domain W3C validator