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 eqid ( PwSer1𝐻 ) = ( PwSer1𝐻 )
12 4 11 5 ply1bas 𝐵 = ( Base ‘ ( 1o mPoly 𝐻 ) )
13 7 9 2 3 10 12 subrgmvrf ( 𝜑 → ( 1o mVar 𝑅 ) : 1o𝐵 )
14 0lt1o ∅ ∈ 1o
15 ffvelrn ( ( ( 1o mVar 𝑅 ) : 1o𝐵 ∧ ∅ ∈ 1o ) → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
16 13 14 15 sylancl ( 𝜑 → ( ( 1o mVar 𝑅 ) ‘ ∅ ) ∈ 𝐵 )
17 6 16 eqeltrid ( 𝜑𝑋𝐵 )