Theorem mhprcl 22066

Description: Reverse closure for homogeneous polynomials, use elfvov1 7441 and elfvov2 7442 with reldmmhp 22060 for the reverse closure of 𝐼 and 𝑅. (Contributed by SN, 4-Aug-2025.)

Hypotheses

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

Assertion

Ref	Expression
mhprcl	⊢ (𝜑 → 𝑁 ∈ ℕ0)

Proof of Theorem mhprcl

Dummy variables 𝑓 𝑔 ℎ 𝑛 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  {crab 3413  Vcvv 3457   ⊆ wss 3924   ↦ cmpt 5198  ^◡ccnv 5650   “ cima 5654  ‘cfv 6527  (class class class)co 7399   supp csupp 8153   ↑_m cmap 8834  Fincfn 8953  ℕcn 12232  ℕ₀cn0 12493  Basecbs 17213   ↾_s cress 17236  0_gc0g 17438   Σ_g cgsu 17439  ℂ_fldccnfld 21300   mPoly cmpl 21851   mHomP cmhp 22052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-1cn 11179  ax-addcl 11181

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7402  df-oprab 7403  df-mpo 7404  df-om 7856  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-nn 12233  df-n0 12494  df-mhp 22059

This theorem is referenced by:  mhpmpl  22067  mhpdeg  22068  mhpmulcl  22072  mhppwdeg  22073  mhpaddcl  22074  mhpinvcl  22075  mhpvscacl  22077  mhpind  42542  mhphf  42545