Metamath Proof Explorer


Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023) Remove sethood hypothesis. (Revised by SN, 18-May-2025)

Ref Expression
Hypotheses mhpinvcl.h 𝐻 = ( 𝐼 mHomP 𝑅 )
mhpinvcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
mhpinvcl.m 𝑀 = ( invg𝑃 )
mhpinvcl.r ( 𝜑𝑅 ∈ Grp )
mhpinvcl.n ( 𝜑𝑁 ∈ ℕ0 )
mhpinvcl.x ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
Assertion mhpinvcl ( 𝜑 → ( 𝑀𝑋 ) ∈ ( 𝐻𝑁 ) )

Proof

Step Hyp Ref Expression
1 mhpinvcl.h 𝐻 = ( 𝐼 mHomP 𝑅 )
2 mhpinvcl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mhpinvcl.m 𝑀 = ( invg𝑃 )
4 mhpinvcl.r ( 𝜑𝑅 ∈ Grp )
5 mhpinvcl.n ( 𝜑𝑁 ∈ ℕ0 )
6 mhpinvcl.x ( 𝜑𝑋 ∈ ( 𝐻𝑁 ) )
7 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 eqid ( 0g𝑅 ) = ( 0g𝑅 )
9 eqid { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
10 reldmmhp Rel dom mHomP
11 10 1 6 elfvov1 ( 𝜑𝐼 ∈ V )
12 2 mplgrp ( ( 𝐼 ∈ V ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
13 11 4 12 syl2anc ( 𝜑𝑃 ∈ Grp )
14 1 2 7 11 4 5 6 mhpmpl ( 𝜑𝑋 ∈ ( Base ‘ 𝑃 ) )
15 7 3 grpinvcl ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑀𝑋 ) ∈ ( Base ‘ 𝑃 ) )
16 13 14 15 syl2anc ( 𝜑 → ( 𝑀𝑋 ) ∈ ( Base ‘ 𝑃 ) )
17 eqid ( invg𝑅 ) = ( invg𝑅 )
18 2 7 17 3 11 4 14 mplneg ( 𝜑 → ( 𝑀𝑋 ) = ( ( invg𝑅 ) ∘ 𝑋 ) )
19 18 oveq1d ( 𝜑 → ( ( 𝑀𝑋 ) supp ( 0g𝑅 ) ) = ( ( ( invg𝑅 ) ∘ 𝑋 ) supp ( 0g𝑅 ) ) )
20 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21 20 17 grpinvfn ( invg𝑅 ) Fn ( Base ‘ 𝑅 )
22 21 a1i ( 𝜑 → ( invg𝑅 ) Fn ( Base ‘ 𝑅 ) )
23 2 20 7 9 14 mplelf ( 𝜑𝑋 : { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
24 ovex ( ℕ0m 𝐼 ) ∈ V
25 24 rabex { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V
26 25 a1i ( 𝜑 → { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∈ V )
27 fvexd ( 𝜑 → ( 0g𝑅 ) ∈ V )
28 8 17 grpinvid ( 𝑅 ∈ Grp → ( ( invg𝑅 ) ‘ ( 0g𝑅 ) ) = ( 0g𝑅 ) )
29 4 28 syl ( 𝜑 → ( ( invg𝑅 ) ‘ ( 0g𝑅 ) ) = ( 0g𝑅 ) )
30 22 23 26 27 29 suppcoss ( 𝜑 → ( ( ( invg𝑅 ) ∘ 𝑋 ) supp ( 0g𝑅 ) ) ⊆ ( 𝑋 supp ( 0g𝑅 ) ) )
31 19 30 eqsstrd ( 𝜑 → ( ( 𝑀𝑋 ) supp ( 0g𝑅 ) ) ⊆ ( 𝑋 supp ( 0g𝑅 ) ) )
32 1 8 9 11 4 5 6 mhpdeg ( 𝜑 → ( 𝑋 supp ( 0g𝑅 ) ) ⊆ { 𝑔 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } )
33 31 32 sstrd ( 𝜑 → ( ( 𝑀𝑋 ) supp ( 0g𝑅 ) ) ⊆ { 𝑔 ∈ { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin } ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } )
34 1 2 7 8 9 11 4 5 16 33 ismhp2 ( 𝜑 → ( 𝑀𝑋 ) ∈ ( 𝐻𝑁 ) )