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

Metamath Proof Explorer

Definition df-mhp

Description: Define the subspaces of order- n homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion df-mhp mHomP = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmhp ⊢ mHomP
1 vi ⊢ 𝑖
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 vn ⊢ 𝑛
5 cn0 ⊢ ℕ0
6 vf ⊢ 𝑓
7 cbs ⊢ Base
8 1 cv ⊢ 𝑖
9 cmpl ⊢ mPoly
10 3 cv ⊢ 𝑟
11 8 10 9 co ⊢ ( 𝑖 mPoly 𝑟 )
12 11 7 cfv ⊢ ( Base ‘ ( 𝑖 mPoly 𝑟 ) )
13 6 cv ⊢ 𝑓
14 csupp ⊢ supp
15 c0g ⊢ 0g
16 10 15 cfv ⊢ ( 0g ‘ 𝑟 )
17 13 16 14 co ⊢ ( 𝑓 supp ( 0g ‘ 𝑟 ) )
18 vg ⊢ 𝑔
19 vh ⊢ ℎ
20 cmap ⊢ ↑m
21 5 8 20 co ⊢ ( ℕ0 ↑m 𝑖 )
22 19 cv ⊢ ℎ
23 22 ccnv ⊢ ◡ ℎ
24 cn ⊢ ℕ
25 23 24 cima ⊢ ( ◡ ℎ “ ℕ )
26 cfn ⊢ Fin
27 25 26 wcel ⊢ ( ◡ ℎ “ ℕ ) ∈ Fin
28 27 19 21 crab ⊢ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
29 ccnfld ⊢ ℂfld
30 cress ⊢ ↾s
31 29 5 30 co ⊢ ( ℂfld ↾s ℕ0 )
32 cgsu ⊢ Σg
33 18 cv ⊢ 𝑔
34 31 33 32 co ⊢ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 )
35 4 cv ⊢ 𝑛
36 34 35 wceq ⊢ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛
37 36 18 28 crab ⊢ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 }
38 17 37 wss ⊢ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 }
39 38 6 12 crab ⊢ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } }
40 4 5 39 cmpt ⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } )
41 1 3 2 2 40 cmpo ⊢ ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
42 0 41 wceq ⊢ mHomP = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )