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

Metamath Proof Explorer

Theorem subrgvr1cl

Description: The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 5-Jul-2015)

Ref Expression
Hypotheses subrgvr1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
subrgvr1.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
subrgvr1.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
subrgvr1cl.u ⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
subrgvr1cl.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
Assertion subrgvr1cl ( 𝜑 → 𝑋 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 subrgvr1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
2 subrgvr1.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
3 subrgvr1.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4 subrgvr1cl.u ⊢ 𝑈 = ( Poly1 ‘ 𝐻 )
5 subrgvr1cl.b ⊢ 𝐵 = ( Base ‘ 𝑈 )
6 1 vr1val ⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
7 eqid ⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
8 1on ⊢ 1o ∈ On
9 8 a1i ⊢ ( 𝜑 → 1o ∈ On )
10 eqid ⊢ ( 1o mPoly 𝐻 ) = ( 1o mPoly 𝐻 )
11 4 5 ply1bas ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
12 7 9 2 3 10 11 subrgmvrf ⊢ ( 𝜑 → ( 1o mVar 𝑅 ) : 1o ⟶ 𝐵 )
13 0lt1o ⊢ ∅ ∈ 1o
14 ffvelcdm ⊢ ( ( ( 1o mVar 𝑅 ) : 1o ⟶ 𝐵 ∧ ∅ ∈ 1o ) → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
15 12 13 14 sylancl ⊢ ( 𝜑 → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
16 6 15 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )