Definition df-elwise

Description: Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers ( axaddf ), so if A and B are sets of complex numbers, then ( A ( elwise+ ) B ) is the set of numbers of the form ( x + y ) with x e. A and y e. B . The set of odd natural numbers is ( ( { 2 } ( elwisex. ) NN0 ) ( elwise+ ) { 1 } ) , or less formally 2 NN0 + 1 . (Contributed by BJ, 22-Dec-2021)

	Ref	Expression
Assertion	df-elwise	|- elwise = ( o e. _V |-> ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		celwise	|- elwise
1		vo	|- o
2		cvv	|- _V
3		vx	|- x
4		vy	|- y
5		vz	|- z
6		vu	|- u
7	3	cv	|- x
8		vv	|- v
9	4	cv	|- y
10	5	cv	|- z
11	6	cv	|- u
12	1	cv	|- o
13	8	cv	|- v
14	11 13 12	co	|- ( u o v )
15	10 14	wceq	|- z = ( u o v )
16	15 8 9	wrex	|- E. v e. y z = ( u o v )
17	16 6 7	wrex	|- E. u e. x E. v e. y z = ( u o v )
18	17 5	cab	|- { z | E. u e. x E. v e. y z = ( u o v ) }
19	3 4 2 2 18	cmpo	|- ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } )
20	1 2 19	cmpt	|- ( o e. _V |-> ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } ) )
21	0 20	wceq	|- elwise = ( o e. _V |-> ( x e. _V , y e. _V |-> { z | E. u e. x E. v e. y z = ( u o v ) } ) )