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	|- B = ( Base ` P )
	0mplric.p	|- P = ( (/) mPoly R )
	0mplric.r	|- ( ph -> R e. Ring )
Assertion	0mplric	|- ( ph -> P ~=r R )

Proof

Step	Hyp	Ref	Expression
1		0mplric.b	|- B = ( Base ` P )
2		0mplric.p	|- P = ( (/) mPoly R )
3		0mplric.r	|- ( ph -> R e. Ring )
4		fveq1	|- ( q = p -> ( q ` (/) ) = ( p ` (/) ) )
5	4	cbvmptv	|- ( q e. B |-> ( q ` (/) ) ) = ( p e. B |-> ( p ` (/) ) )
6	1 2 3 5	0mplrim	|- ( ph -> ( q e. B |-> ( q ` (/) ) ) e. ( P RingIso R ) )
7		brrici	|- ( ( q e. B |-> ( q ` (/) ) ) e. ( P RingIso R ) -> P ~=r R )
8	6 7	syl	|- ( ph -> P ~=r R )