This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mvr

Description: Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015)

Ref Expression
Assertion df-mvr mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmvr ⊢ mVar
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 vx ⊢ 𝑥
5 1 cv ⊢ 𝑖
6 vf ⊢ 𝑓
7 vh ⊢ ℎ
8 cn0 ⊢ ℕ0
9 cmap ⊢ ↑m
10 8 5 9 co ⊢ ( ℕ0 ↑m 𝑖 )
11 7 cv ⊢ ℎ
12 11 ccnv ⊢ ◡ ℎ
13 cn ⊢ ℕ
14 12 13 cima ⊢ ( ◡ ℎ “ ℕ )
15 cfn ⊢ Fin
16 14 15 wcel ⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
17 16 7 10 crab ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
18 6 cv ⊢ 𝑓
19 vy ⊢ 𝑦
20 19 cv ⊢ 𝑦
21 4 cv ⊢ 𝑥
22 20 21 wceq ⊢ 𝑦 = 𝑥
23 c1 ⊢ 1
24 cc0 ⊢ 0
25 22 23 24 cif ⊢ if ( 𝑦 = 𝑥 , 1 , 0 )
26 19 5 25 cmpt ⊢ ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) )
27 18 26 wceq ⊢ 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) )
28 cur ⊢ 1r
29 3 cv ⊢ 𝑟
30 29 28 cfv ⊢ ( 1r ‘ 𝑟 )
31 c0g ⊢ 0g
32 29 31 cfv ⊢ ( 0g ‘ 𝑟 )
33 27 30 32 cif ⊢ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) )
34 6 17 33 cmpt ⊢ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) )
35 4 5 34 cmpt ⊢ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) )
36 1 3 2 2 35 cmpo ⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )
37 0 36 wceq ⊢ mVar = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑥 ∈ 𝑖 ↦ ( 𝑓 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 𝑖 ↦ if ( 𝑦 = 𝑥 , 1 , 0 ) ) , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) ) ) )