Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-elwise Structured version   Visualization version   GIF version

Definition df-elwise 35364
Description: Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 11002), so if 𝐴 and 𝐡 are sets of complex numbers, then (𝐴(elwiseβ€˜ + )𝐡) is the set of numbers of the form (π‘₯ + 𝑦) with π‘₯ ∈ 𝐴 and 𝑦 ∈ 𝐡. The set of odd natural numbers is (({2}(elwiseβ€˜ Β· )β„•0)(elwiseβ€˜ + ){1}), or less formally 2β„•0 + 1. (Contributed by BJ, 22-Dec-2021.)
Assertion
Ref Expression
df-elwise elwise = (π‘œ ∈ V ↦ (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ βˆƒπ‘’ ∈ π‘₯ βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)}))
Distinct variable group:   π‘₯,π‘œ,𝑦,𝑧,𝑒,𝑣

Detailed syntax breakdown of Definition df-elwise
StepHypRef Expression
1 celwise 35363 . 2 class elwise
2 vo . . 3 setvar π‘œ
3 cvv 3441 . . 3 class V
4 vx . . . 4 setvar π‘₯
5 vy . . . 4 setvar 𝑦
6 vz . . . . . . . . 9 setvar 𝑧
76cv 1539 . . . . . . . 8 class 𝑧
8 vu . . . . . . . . . 10 setvar 𝑒
98cv 1539 . . . . . . . . 9 class 𝑒
10 vv . . . . . . . . . 10 setvar 𝑣
1110cv 1539 . . . . . . . . 9 class 𝑣
122cv 1539 . . . . . . . . 9 class π‘œ
139, 11, 12co 7337 . . . . . . . 8 class (π‘’π‘œπ‘£)
147, 13wceq 1540 . . . . . . 7 wff 𝑧 = (π‘’π‘œπ‘£)
155cv 1539 . . . . . . 7 class 𝑦
1614, 10, 15wrex 3070 . . . . . 6 wff βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)
174cv 1539 . . . . . 6 class π‘₯
1816, 8, 17wrex 3070 . . . . 5 wff βˆƒπ‘’ ∈ π‘₯ βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)
1918, 6cab 2713 . . . 4 class {𝑧 ∣ βˆƒπ‘’ ∈ π‘₯ βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)}
204, 5, 3, 3, 19cmpo 7339 . . 3 class (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ βˆƒπ‘’ ∈ π‘₯ βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)})
212, 3, 20cmpt 5175 . 2 class (π‘œ ∈ V ↦ (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ βˆƒπ‘’ ∈ π‘₯ βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)}))
221, 21wceq 1540 1 wff elwise = (π‘œ ∈ V ↦ (π‘₯ ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ βˆƒπ‘’ ∈ π‘₯ βˆƒπ‘£ ∈ 𝑦 𝑧 = (π‘’π‘œπ‘£)}))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator