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

Definition df-imas 14438
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 4848, 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 4847) and/or ( with df-ress 14173) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.)

Assertion
Ref Expression
df-imas
Distinct variable group:   , , , , , , , , , ,

Detailed syntax breakdown of Definition df-imas
StepHypRef Expression
1 cimas 14434 . 2
2 vf . . 3
3 vr . . 3
4 cvv 2967 . . 3
5 vv . . . 4
63cv 1368 . . . . 5
7 cbs 14166 . . . . 5
86, 7cfv 5413 . . . 4
9 cnx 14163 . . . . . . . . 9
109, 7cfv 5413 . . . . . . . 8
112cv 1368 . . . . . . . . 9
1211crn 4836 . . . . . . . 8
1310, 12cop 3878 . . . . . . 7
14 cplusg 14230 . . . . . . . . 9
159, 14cfv 5413 . . . . . . . 8
16 vp . . . . . . . . 9
175cv 1368 . . . . . . . . 9
18 vq . . . . . . . . . 10
1916cv 1368 . . . . . . . . . . . . . 14
2019, 11cfv 5413 . . . . . . . . . . . . 13
2118cv 1368 . . . . . . . . . . . . . 14
2221, 11cfv 5413 . . . . . . . . . . . . 13
2320, 22cop 3878 . . . . . . . . . . . 12
246, 14cfv 5413 . . . . . . . . . . . . . 14
2519, 21, 24co 6086 . . . . . . . . . . . . 13
2625, 11cfv 5413 . . . . . . . . . . . 12
2723, 26cop 3878 . . . . . . . . . . 11
2827csn 3872 . . . . . . . . . 10
2918, 17, 28ciun 4166 . . . . . . . . 9
3016, 17, 29ciun 4166 . . . . . . . 8
3115, 30cop 3878 . . . . . . 7
32 cmulr 14231 . . . . . . . . 9
339, 32cfv 5413 . . . . . . . 8
346, 32cfv 5413 . . . . . . . . . . . . . 14
3519, 21, 34co 6086 . . . . . . . . . . . . 13
3635, 11cfv 5413 . . . . . . . . . . . 12
3723, 36cop 3878 . . . . . . . . . . 11
3837csn 3872 . . . . . . . . . 10
3918, 17, 38ciun 4166 . . . . . . . . 9
4016, 17, 39ciun 4166 . . . . . . . 8
4133, 40cop 3878 . . . . . . 7
4213, 31, 41ctp 3876 . . . . . 6
43 csca 14233 . . . . . . . . 9
449, 43cfv 5413 . . . . . . . 8
456, 43cfv 5413 . . . . . . . 8
4644, 45cop 3878 . . . . . . 7
47 cvsca 14234 . . . . . . . . 9
489, 47cfv 5413 . . . . . . . 8
49 vx . . . . . . . . . 10
5045, 7cfv 5413 . . . . . . . . . 10
5122csn 3872 . . . . . . . . . 10
526, 47cfv 5413 . . . . . . . . . . . 12
5319, 21, 52co 6086 . . . . . . . . . . 11
5453, 11cfv 5413 . . . . . . . . . 10
5516, 49, 50, 51, 54cmpt2 6088 . . . . . . . . 9
5618, 17, 55ciun 4166 . . . . . . . 8
5748, 56cop 3878 . . . . . . 7
58 cip 14235 . . . . . . . . 9
599, 58cfv 5413 . . . . . . . 8
606, 58cfv 5413 . . . . . . . . . . . . 13
6119, 21, 60co 6086 . . . . . . . . . . . 12
6223, 61cop 3878 . . . . . . . . . . 11
6362csn 3872 . . . . . . . . . 10
6418, 17, 63ciun 4166 . . . . . . . . 9
6516, 17, 64ciun 4166 . . . . . . . 8
6659, 65cop 3878 . . . . . . 7
6746, 57, 66ctp 3876 . . . . . 6
6842, 67cun 3321 . . . . 5
69 cts 14236 . . . . . . . 8
709, 69cfv 5413 . . . . . . 7
71 ctopn 14352 . . . . . . . . 9
726, 71cfv 5413 . . . . . . . 8
73 cqtop 14433 . . . . . . . 8
7472, 11, 73co 6086 . . . . . . 7
7570, 74cop 3878 . . . . . 6
76 cple 14237 . . . . . . . 8
779, 76cfv 5413 . . . . . . 7
786, 76cfv 5413 . . . . . . . . 9
7911, 78ccom 4839 . . . . . . . 8
8011ccnv 4834 . . . . . . . 8
8179, 80ccom 4839 . . . . . . 7
8277, 81cop 3878 . . . . . 6
83 cds 14239 . . . . . . . 8
849, 83cfv 5413 . . . . . . 7
85 vy . . . . . . . 8
86 vn . . . . . . . . . 10
87 cn 10314 . . . . . . . . . 10
88 vg . . . . . . . . . . . 12
89 c1 9275 . . . . . . . . . . . . . . . . . 18
90 vh . . . . . . . . . . . . . . . . . . 19
9190cv 1368 . . . . . . . . . . . . . . . . . 18
9289, 91cfv 5413 . . . . . . . . . . . . . . . . 17
93 c1st 6570 . . . . . . . . . . . . . . . . 17
9492, 93cfv 5413 . . . . . . . . . . . . . . . 16
9594, 11cfv 5413 . . . . . . . . . . . . . . 15
9649cv 1368 . . . . . . . . . . . . . . 15
9795, 96wceq 1369 . . . . . . . . . . . . . 14
9886cv 1368 . . . . . . . . . . . . . . . . . 18
9998, 91cfv 5413 . . . . . . . . . . . . . . . . 17
100 c2nd 6571 . . . . . . . . . . . . . . . . 17
10199, 100cfv 5413 . . . . . . . . . . . . . . . 16
102101, 11cfv 5413 . . . . . . . . . . . . . . 15
10385cv 1368 . . . . . . . . . . . . . . 15
104102, 103wceq 1369 . . . . . . . . . . . . . 14
105 vi . . . . . . . . . . . . . . . . . . . 20
106105cv 1368 . . . . . . . . . . . . . . . . . . 19
107106, 91cfv 5413 . . . . . . . . . . . . . . . . . 18
108107, 100cfv 5413 . . . . . . . . . . . . . . . . 17
109108, 11cfv 5413 . . . . . . . . . . . . . . . 16
110 caddc 9277 . . . . . . . . . . . . . . . . . . . 20
111106, 89, 110co 6086 . . . . . . . . . . . . . . . . . . 19
112111, 91cfv 5413 . . . . . . . . . . . . . . . . . 18
113112, 93cfv 5413 . . . . . . . . . . . . . . . . 17
114113, 11cfv 5413 . . . . . . . . . . . . . . . 16
115109, 114wceq 1369 . . . . . . . . . . . . . . 15
116 cmin 9587 . . . . . . . . . . . . . . . . 17
11798, 89, 116co 6086 . . . . . . . . . . . . . . . 16
118 cfz 11429 . . . . . . . . . . . . . . . 16
11989, 117, 118co 6086 . . . . . . . . . . . . . . 15
120115, 105, 119wral 2710 . . . . . . . . . . . . . 14
12197, 104, 120w3a 965 . . . . . . . . . . . . 13
12217, 17cxp 4833 . . . . . . . . . . . . . 14
12389, 98, 118co 6086 . . . . . . . . . . . . . 14
124 cmap 7206 . . . . . . . . . . . . . 14
125122, 123, 124co 6086 . . . . . . . . . . . . 13
126121, 90, 125crab 2714 . . . . . . . . . . . 12
127 cxrs 14430 . . . . . . . . . . . . 13
1286, 83cfv 5413 . . . . . . . . . . . . . 14
12988cv 1368 . . . . . . . . . . . . . 14
130128, 129ccom 4839 . . . . . . . . . . . . 13
131 cgsu 14371 . . . . . . . . . . . . 13
132127, 130, 131co 6086 . . . . . . . . . . . 12
13388, 126, 132cmpt 4345 . . . . . . . . . . 11
134133crn 4836 . . . . . . . . . 10
13586, 87, 134ciun 4166 . . . . . . . . 9
136 cxr 9409 . . . . . . . . 9
137 clt 9410 . . . . . . . . . 10
138137ccnv 4834 . . . . . . . . 9
139135, 136, 138csup 7682 . . . . . . . 8
14049, 85, 12, 12, 139cmpt2 6088 . . . . . . 7
14184, 140cop 3878 . . . . . 6
14275, 82, 141ctp 3876 . . . . 5
14368, 142cun 3321 . . . 4
1445, 8, 143csb 3283 . . 3
1452, 3, 4, 4, 144cmpt2 6088 . 2
1461, 145wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  imasval  14441
  Copyright terms: Public domain W3C validator