Theorem mhprcl

Description: Reverse closure for homogeneous polynomials, use elfvov1 and elfvov2 with reldmmhp for the reverse closure of I and R . (Contributed by SN, 4-Aug-2025)

	Ref	Expression
Hypotheses	mhprcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
	mhprcl.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
Assertion	mhprcl	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		mhprcl.h	⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
2		mhprcl.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) )
3		eqid	⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
4		eqid	⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6		eqid	⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
7		reldmmhp	⊢ Rel dom mHomP
8	7 1 2	elfvov1	⊢ ( 𝜑 → 𝐼 ∈ V )
9	7 1 2	elfvov2	⊢ ( 𝜑 → 𝑅 ∈ V )
10	1 3 4 5 6 8 9	mhpfval	⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) )
11	10	fveq1d	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑁 ) = ( ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) ‘ 𝑁 ) )
12	2 11	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) ‘ 𝑁 ) )
13		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } )
14	13	mptrcl	⊢ ( 𝑋 ∈ ( ( 𝑛 ∈ ℕ0 ↦ { 𝑓 ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∣ ( 𝑓 supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑛 } } ) ‘ 𝑁 ) → 𝑁 ∈ ℕ0 )
15	12 14	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )