This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ⊢ ( 𝜑 → 𝑋 : { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
23 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
24 23 rabex ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∈ V
25 24 a1i ⊢ ( 𝜑 → { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ 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 ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
32 30 31 sstrd ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑋 ) supp ( 0g ‘ 𝑅 ) ) ⊆ { 𝑔 ∈ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } )
33 1 2 6 7 8 9 15 32 ismhp2 ⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) ∈ ( 𝐻 ‘ 𝑁 ) )