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 34442
 Description: Define the elementwise operation associated with a given operation. For instance, + is the addition of complex numbers (axaddf 10565), 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 34441 . 2 class elwise
2 vo . . 3 setvar 𝑜
3 cvv 3480 . . 3 class V
4 vx . . . 4 setvar 𝑥
5 vy . . . 4 setvar 𝑦
6 vz . . . . . . . . 9 setvar 𝑧
76cv 1537 . . . . . . . 8 class 𝑧
8 vu . . . . . . . . . 10 setvar 𝑢
98cv 1537 . . . . . . . . 9 class 𝑢
10 vv . . . . . . . . . 10 setvar 𝑣
1110cv 1537 . . . . . . . . 9 class 𝑣
122cv 1537 . . . . . . . . 9 class 𝑜
139, 11, 12co 7149 . . . . . . . 8 class (𝑢𝑜𝑣)
147, 13wceq 1538 . . . . . . 7 wff 𝑧 = (𝑢𝑜𝑣)
155cv 1537 . . . . . . 7 class 𝑦
1614, 10, 15wrex 3134 . . . . . 6 wff 𝑣𝑦 𝑧 = (𝑢𝑜𝑣)
174cv 1537 . . . . . 6 class 𝑥
1816, 8, 17wrex 3134 . . . . 5 wff 𝑢𝑥𝑣𝑦 𝑧 = (𝑢𝑜𝑣)
1918, 6cab 2802 . . . 4 class {𝑧 ∣ ∃𝑢𝑥𝑣𝑦 𝑧 = (𝑢𝑜𝑣)}
204, 5, 3, 3, 19cmpo 7151 . . 3 class (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢𝑥𝑣𝑦 𝑧 = (𝑢𝑜𝑣)})
212, 3, 20cmpt 5132 . 2 class (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢𝑥𝑣𝑦 𝑧 = (𝑢𝑜𝑣)}))
221, 21wceq 1538 1 wff elwise = (𝑜 ∈ V ↦ (𝑥 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∣ ∃𝑢𝑥𝑣𝑦 𝑧 = (𝑢𝑜𝑣)}))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator