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

Metamath Proof Explorer

Theorem mplelbas

Description: Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015) (Revised by AV, 25-Jun-2019)

Ref Expression
Hypotheses mplval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
mplval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
mplval.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplbas.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
Assertion mplelbas ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 finSupp 0 ) )

Proof

Step Hyp Ref Expression
1 mplval.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplval.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3 mplval.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
4 mplval.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 mplbas.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
6 breq1 ⊢ ( 𝑓 = 𝑋 → ( 𝑓 finSupp 0 ↔ 𝑋 finSupp 0 ) )
7 1 2 3 4 5 mplbas ⊢ 𝑈 = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }
8 6 7 elrab2 ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑋 finSupp 0 ) )