Definition df-iimas 13004

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 f must either be injective or satisfy the well-definedness condition f ( a ) = f ( c ) /\ f ( b ) = f ( d ) -> f ( a + b ) = f ( c + d ) for each relevant operation.

Note that although we call this an "image" by association to df-ima 4677, in order to keep the definition simple we consider only the case when the domain of F is equal to the base set of R. Other cases can be achieved by restricting F (with df-res 4676) and/or R ( with df-iress 12711) to their common domain. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by AV, 6-Oct-2020.)

Assertion

Ref	Expression
df-iimas	|- "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } )

Distinct variable group:   f, p, q, r, v

Detailed syntax breakdown of Definition df-iimas

Step	Hyp	Ref	Expression
1		cimas 13001	. 2 class "s
2		vf	. . 3 setvar f
3		vr	. . 3 setvar r
4		cvv 2763	. . 3 class _V
5		vv	. . . 4 setvar v
6	3	cv 1363	. . . . 5 class r
7		cbs 12703	. . . . 5 class Base
8	6, 7	cfv 5259	. . . 4 class ( Base ` r )
9		cnx 12700	. . . . . . 7 class ndx
10	9, 7	cfv 5259	. . . . . 6 class ( Base ` ndx )
11	2	cv 1363	. . . . . . 7 class f
12	11	crn 4665	. . . . . 6 class ran f
13	10, 12	cop 3626	. . . . 5 class <. ( Base ` ndx ) , ran f >.
14		cplusg 12780	. . . . . . 7 class +g
15	9, 14	cfv 5259	. . . . . 6 class ( +g ` ndx )
16		vp	. . . . . . 7 setvar p
17	5	cv 1363	. . . . . . 7 class v
18		vq	. . . . . . . 8 setvar q
19	16	cv 1363	. . . . . . . . . . . 12 class p
20	19, 11	cfv 5259	. . . . . . . . . . 11 class ( f ` p )
21	18	cv 1363	. . . . . . . . . . . 12 class q
22	21, 11	cfv 5259	. . . . . . . . . . 11 class ( f ` q )
23	20, 22	cop 3626	. . . . . . . . . 10 class <. ( f ` p ) , ( f ` q ) >.
24	6, 14	cfv 5259	. . . . . . . . . . . 12 class ( +g ` r )
25	19, 21, 24	co 5925	. . . . . . . . . . 11 class ( p ( +g ` r ) q )
26	25, 11	cfv 5259	. . . . . . . . . 10 class ( f ` ( p ( +g ` r ) q ) )
27	23, 26	cop 3626	. . . . . . . . 9 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >.
28	27	csn 3623	. . . . . . . 8 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
29	18, 17, 28	ciun 3917	. . . . . . 7 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
30	16, 17, 29	ciun 3917	. . . . . 6 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. }
31	15, 30	cop 3626	. . . . 5 class <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >.
32		cmulr 12781	. . . . . . 7 class .r
33	9, 32	cfv 5259	. . . . . 6 class ( .r ` ndx )
34	6, 32	cfv 5259	. . . . . . . . . . . 12 class ( .r ` r )
35	19, 21, 34	co 5925	. . . . . . . . . . 11 class ( p ( .r ` r ) q )
36	35, 11	cfv 5259	. . . . . . . . . 10 class ( f ` ( p ( .r ` r ) q ) )
37	23, 36	cop 3626	. . . . . . . . 9 class <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >.
38	37	csn 3623	. . . . . . . 8 class { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
39	18, 17, 38	ciun 3917	. . . . . . 7 class U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
40	16, 17, 39	ciun 3917	. . . . . 6 class U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. }
41	33, 40	cop 3626	. . . . 5 class <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >.
42	13, 31, 41	ctp 3625	. . . 4 class { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. }
43	5, 8, 42	csb 3084	. . 3 class [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. }
44	2, 3, 4, 4, 43	cmpo 5927	. 2 class ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } )
45	1, 44	wceq 1364	1 wff "s = ( f e. _V , r e. _V |-> [_ ( Base ` r ) / v ]_ { <. ( Base ` ndx ) , ran f >. , <. ( +g ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( +g ` r ) q ) ) >. } >. , <. ( .r ` ndx ) , U_ p e. v U_ q e. v { <. <. ( f ` p ) , ( f ` q ) >. , ( f ` ( p ( .r ` r ) q ) ) >. } >. } )

This definition is referenced by:  imasex  13007  imasival  13008