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

Metamath Proof Explorer

Theorem mhpfval

Description: Value of the "homogeneous polynomial" operator. (Contributed by Steven Nguyen, 25-Aug-2023)

Ref Expression
Hypotheses mhpfval.h ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
mhpfval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mhpfval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mhpfval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
mhpfval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
mhpfval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mhpfval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
Assertion mhpfval ( 𝜑 → 𝐻 = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )

Proof

Step Hyp Ref Expression
1 mhpfval.h ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2 mhpfval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mhpfval.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 mhpfval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 mhpfval.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
6 mhpfval.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7 mhpfval.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
8 6 elexd ⊢ ( 𝜑 → 𝐼 ∈ V )
9 7 elexd ⊢ ( 𝜑 → 𝑅 ∈ V )
10 oveq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPoly 𝑟 ) = ( 𝐼 mPoly 𝑅 ) )
11 10 2 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑖 mPoly 𝑟 ) = 𝑃 )
12 11 fveq2d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = ( Base ‘ 𝑃 ) )
13 12 3 eqtr4di ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) = 𝐵 )
14 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
15 14 4 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
16 15 oveq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑓 supp ( 0g ‘ 𝑟 ) ) = ( 𝑓 supp 0 ) )
17 16 adantl ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑓 supp ( 0g ‘ 𝑟 ) ) = ( 𝑓 supp 0 ) )
18 oveq2 ⊢ ( 𝑖 = 𝐼 → ( ℕ0 ↑m 𝑖 ) = ( ℕ0 ↑m 𝐼 ) )
19 18 rabeqdv ⊢ ( 𝑖 = 𝐼 → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } )
20 19 5 eqtr4di ⊢ ( 𝑖 = 𝐼 → { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = 𝐷 )
21 20 rabeqdv ⊢ ( 𝑖 = 𝐼 → { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } )
22 21 adantr ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } = { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } )
23 17 22 sseq12d ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } ↔ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } ) )
24 13 23 rabeqbidv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } )
25 24 mpteq2dv ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑟 = 𝑅 ) → ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
26 df-mhp ⊢ mHomP = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝑖 mPoly 𝑟 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑟 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝑖 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
27 nn0ex ⊢ ℕ0 ∈ V
28 27 mptex ⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) ∈ V
29 25 26 28 ovmpoa ⊢ ( ( 𝐼 ∈ V ∧ 𝑅 ∈ V ) → ( 𝐼 mHomP 𝑅 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
30 8 9 29 syl2anc ⊢ ( 𝜑 → ( 𝐼 mHomP 𝑅 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
31 1 30 eqtrid ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ 𝐵 ∣ ( 𝑓 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )