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 ⊢ X = var 1 ⁡ R
subrgvr1.r ⊢ φ → T ∈ SubRing ⁡ R
subrgvr1.h ⊢ H = R ↾ 𝑠 T
Assertion subrgvr1 ⊢ φ → X = var 1 ⁡ H

Proof

Step Hyp Ref Expression
1 subrgvr1.x ⊢ X = var 1 ⁡ R
2 subrgvr1.r ⊢ φ → T ∈ SubRing ⁡ R
3 subrgvr1.h ⊢ H = R ↾ 𝑠 T
4 eqid ⊢ 1 𝑜 mVar R = 1 𝑜 mVar R
5 1on ⊢ 1 𝑜 ∈ On
6 5 a1i ⊢ φ → 1 𝑜 ∈ On
7 4 6 2 3 subrgmvr ⊢ φ → 1 𝑜 mVar R = 1 𝑜 mVar H
8 7 fveq1d ⊢ φ → 1 𝑜 mVar R ⁡ ∅ = 1 𝑜 mVar H ⁡ ∅
9 1 vr1val ⊢ X = 1 𝑜 mVar R ⁡ ∅
10 eqid ⊢ var 1 ⁡ H = var 1 ⁡ H
11 10 vr1val ⊢ var 1 ⁡ H = 1 𝑜 mVar H ⁡ ∅
12 8 9 11 3eqtr4g ⊢ φ → X = var 1 ⁡ H