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 𝑔 ) = 𝑛 } } ) )