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

Metamath Proof Explorer

Theorem vr1cl

Description: The generator of a univariate polynomial algebra is contained in the base set. (Contributed by Stefan O'Rear, 19-Mar-2015)

Ref Expression
Hypotheses vr1cl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
vr1cl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
vr1cl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 vr1cl.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
2 vr1cl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 vr1cl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 1 vr1val ⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
5 eqid ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6 eqid ⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
7 2 3 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
8 1onn ⊢ 1o ∈ ω
9 8 a1i ⊢ ( 𝑅 ∈ Ring → 1o ∈ ω )
10 id ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
11 0lt1o ⊢ ∅ ∈ 1o
12 11 a1i ⊢ ( 𝑅 ∈ Ring → ∅ ∈ 1o )
13 5 6 7 9 10 12 mvrcl ⊢ ( 𝑅 ∈ Ring → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
14 4 13 eqeltrid ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )