Theorem mplneg

Description: The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024)

	Ref	Expression
Hypotheses	mplneg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplneg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplneg.n	⊢ 𝑁 = ( invg ‘ 𝑅 )
	mplneg.m	⊢ 𝑀 = ( invg ‘ 𝑃 )
	mplneg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplneg.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
	mplneg.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion	mplneg	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) = ( 𝑁 ∘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		mplneg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplneg.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		mplneg.n	⊢ 𝑁 = ( invg ‘ 𝑅 )
4		mplneg.m	⊢ 𝑀 = ( invg ‘ 𝑃 )
5		mplneg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		mplneg.r	⊢ ( 𝜑 → 𝑅 ∈ Grp )
7		mplneg.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
9	8 1 2 5 6	mplsubg	⊢ ( 𝜑 → 𝐵 ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
10	1 8 2	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s 𝐵 )
11		eqid	⊢ ( invg ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( invg ‘ ( 𝐼 mPwSer 𝑅 ) )
12	10 11 4	subginv	⊢ ( ( 𝐵 ∈ ( SubGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ ( 𝐼 mPwSer 𝑅 ) ) ‘ 𝑋 ) = ( 𝑀 ‘ 𝑋 ) )
13	9 7 12	syl2anc	⊢ ( 𝜑 → ( ( invg ‘ ( 𝐼 mPwSer 𝑅 ) ) ‘ 𝑋 ) = ( 𝑀 ‘ 𝑋 ) )
14		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
15		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
16	1 8 2 15	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
17	16	sseli	⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
18	7 17	syl	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
19	8 5 6 14 3 15 11 18	psrneg	⊢ ( 𝜑 → ( ( invg ‘ ( 𝐼 mPwSer 𝑅 ) ) ‘ 𝑋 ) = ( 𝑁 ∘ 𝑋 ) )
20	13 19	eqtr3d	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑋 ) = ( 𝑁 ∘ 𝑋 ) )