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

Metamath Proof Explorer

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 ⊢ φ → R ∈ Ring
Assertion 0mplric ⊢ φ → P ≃ 𝑟 R

Proof

Step Hyp Ref Expression
1 0mplric.b ⊢ B = Base P
2 0mplric.p ⊢ P = ∅ mPoly R
3 0mplric.r ⊢ φ → R ∈ Ring
4 fveq1 ⊢ q = p → q ⁡ ∅ = p ⁡ ∅
5 4 cbvmptv ⊢ q ∈ B ⟼ q ⁡ ∅ = p ∈ B ⟼ p ⁡ ∅
6 1 2 3 5 0mplrim ⊢ φ → q ∈ B ⟼ q ⁡ ∅ ∈ P RingIso R
7 brrici ⊢ q ∈ B ⟼ q ⁡ ∅ ∈ P RingIso R → P ≃ 𝑟 R
8 6 7 syl ⊢ φ → P ≃ 𝑟 R