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