MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mvr Structured version   Visualization version   GIF version

Definition df-mvr 19405
Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.)
Assertion
Ref Expression
df-mvr mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r𝑟), (0g𝑟)))))
Distinct variable group:   𝑓,,𝑖,𝑟,𝑥,𝑦

Detailed syntax breakdown of Definition df-mvr
StepHypRef Expression
1 cmvr 19400 . 2 class mVar
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3231 . . 3 class V
5 vx . . . 4 setvar 𝑥
62cv 1522 . . . 4 class 𝑖
7 vf . . . . 5 setvar 𝑓
8 vh . . . . . . . . . 10 setvar
98cv 1522 . . . . . . . . 9 class
109ccnv 5142 . . . . . . . 8 class
11 cn 11058 . . . . . . . 8 class
1210, 11cima 5146 . . . . . . 7 class ( “ ℕ)
13 cfn 7997 . . . . . . 7 class Fin
1412, 13wcel 2030 . . . . . 6 wff ( “ ℕ) ∈ Fin
15 cn0 11330 . . . . . . 7 class 0
16 cmap 7899 . . . . . . 7 class 𝑚
1715, 6, 16co 6690 . . . . . 6 class (ℕ0𝑚 𝑖)
1814, 8, 17crab 2945 . . . . 5 class { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin}
197cv 1522 . . . . . . 7 class 𝑓
20 vy . . . . . . . 8 setvar 𝑦
2120, 5weq 1931 . . . . . . . . 9 wff 𝑦 = 𝑥
22 c1 9975 . . . . . . . . 9 class 1
23 cc0 9974 . . . . . . . . 9 class 0
2421, 22, 23cif 4119 . . . . . . . 8 class if(𝑦 = 𝑥, 1, 0)
2520, 6, 24cmpt 4762 . . . . . . 7 class (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
2619, 25wceq 1523 . . . . . 6 wff 𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0))
273cv 1522 . . . . . . 7 class 𝑟
28 cur 18547 . . . . . . 7 class 1r
2927, 28cfv 5926 . . . . . 6 class (1r𝑟)
30 c0g 16147 . . . . . . 7 class 0g
3127, 30cfv 5926 . . . . . 6 class (0g𝑟)
3226, 29, 31cif 4119 . . . . 5 class if(𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r𝑟), (0g𝑟))
337, 18, 32cmpt 4762 . . . 4 class (𝑓 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r𝑟), (0g𝑟)))
345, 6, 33cmpt 4762 . . 3 class (𝑥𝑖 ↦ (𝑓 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r𝑟), (0g𝑟))))
352, 3, 4, 4, 34cmpt2 6692 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r𝑟), (0g𝑟)))))
361, 35wceq 1523 1 wff mVar = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥𝑖 ↦ (𝑓 ∈ { ∈ (ℕ0𝑚 𝑖) ∣ ( “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r𝑟), (0g𝑟)))))
Colors of variables: wff setvar class
This definition is referenced by:  mvrfval  19468  vr1val  19610
  Copyright terms: Public domain W3C validator