Metamath Proof Explorer


Theorem mhpinvcl

Description: Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023) Remove closure hypotheses. (Revised by SN, 4-Sep-2025)

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