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

Metamath Proof Explorer

Theorem subrgvr1

Description: The variables in a subring polynomial algebra are the same as the original ring. (Contributed by Mario Carneiro, 5-Jul-2015)

Ref Expression
Hypotheses subrgvr1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
subrgvr1.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
subrgvr1.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
Assertion subrgvr1 ( 𝜑 → 𝑋 = ( var1 ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 subrgvr1.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
2 subrgvr1.r ⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
3 subrgvr1.h ⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
4 eqid ⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
5 1on ⊢ 1o ∈ On
6 5 a1i ⊢ ( 𝜑 → 1o ∈ On )
7 4 6 2 3 subrgmvr ⊢ ( 𝜑 → ( 1o mVar 𝑅 ) = ( 1o mVar 𝐻 ) )
8 7 fveq1d ⊢ ( 𝜑 → ( ( 1o mVar 𝑅 ) ‘ ∅ ) = ( ( 1o mVar 𝐻 ) ‘ ∅ ) )
9 1 vr1val ⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
10 eqid ⊢ ( var1 ‘ 𝐻 ) = ( var1 ‘ 𝐻 )
11 10 vr1val ⊢ ( var1 ‘ 𝐻 ) = ( ( 1o mVar 𝐻 ) ‘ ∅ )
12 8 9 11 3eqtr4g ⊢ ( 𝜑 → 𝑋 = ( var1 ‘ 𝐻 ) )