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 
|- X = ( var1 ` R )
subrgvr1.r 
|- ( ph -> T e. ( SubRing ` R ) )
subrgvr1.h 
|- H = ( R |`s T )
subrgvr1cl.u 
|- U = ( Poly1 ` H )
subrgvr1cl.b 
|- B = ( Base ` U )
Assertion subrgvr1cl 
|- ( ph -> X e. B )

Proof

Step Hyp Ref Expression
1 subrgvr1.x 
 |-  X = ( var1 ` R )
2 subrgvr1.r 
 |-  ( ph -> T e. ( SubRing ` R ) )
3 subrgvr1.h 
 |-  H = ( R |`s T )
4 subrgvr1cl.u 
 |-  U = ( Poly1 ` H )
5 subrgvr1cl.b 
 |-  B = ( Base ` U )
6 1 vr1val 
 |-  X = ( ( 1o mVar R ) ` (/) )
7 eqid 
 |-  ( 1o mVar R ) = ( 1o mVar R )
8 1on 
 |-  1o e. On
9 8 a1i 
 |-  ( ph -> 1o e. On )
10 eqid 
 |-  ( 1o mPoly H ) = ( 1o mPoly H )
11 4 5 ply1bas 
 |-  B = ( Base ` ( 1o mPoly H ) )
12 7 9 2 3 10 11 subrgmvrf 
 |-  ( ph -> ( 1o mVar R ) : 1o --> B )
13 0lt1o 
 |-  (/) e. 1o
14 ffvelcdm 
 |-  ( ( ( 1o mVar R ) : 1o --> B /\ (/) e. 1o ) -> ( ( 1o mVar R ) ` (/) ) e. B )
15 12 13 14 sylancl 
 |-  ( ph -> ( ( 1o mVar R ) ` (/) ) e. B )
16 6 15 eqeltrid 
 |-  ( ph -> X e. B )