Theorem 0mplric

Description: Multivariate polynomials with no variables are isomorphic with the underlying ring. (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	0mplric.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	0mplric.p	⊢ 𝑃 = ( ∅ mPoly 𝑅 )
	0mplric.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	0mplric	⊢ ( 𝜑 → 𝑃 ≃𝑟 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		0mplric.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
2		0mplric.p	⊢ 𝑃 = ( ∅ mPoly 𝑅 )
3		0mplric.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		fveq1	⊢ ( 𝑞 = 𝑝 → ( 𝑞 ‘ ∅ ) = ( 𝑝 ‘ ∅ ) )
5	4	cbvmptv	⊢ ( 𝑞 ∈ 𝐵 ↦ ( 𝑞 ‘ ∅ ) ) = ( 𝑝 ∈ 𝐵 ↦ ( 𝑝 ‘ ∅ ) )
6	1 2 3 5	0mplrim	⊢ ( 𝜑 → ( 𝑞 ∈ 𝐵 ↦ ( 𝑞 ‘ ∅ ) ) ∈ ( 𝑃 RingIso 𝑅 ) )
7		brrici	⊢ ( ( 𝑞 ∈ 𝐵 ↦ ( 𝑞 ‘ ∅ ) ) ∈ ( 𝑃 RingIso 𝑅 ) → 𝑃 ≃𝑟 𝑅 )
8	6 7	syl	⊢ ( 𝜑 → 𝑃 ≃𝑟 𝑅 )