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

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 subrgvr1cl.u ⊢ U = Poly 1 ⁡ H
5 subrgvr1cl.b ⊢ B = Base U
6 1 vr1val ⊢ X = 1 𝑜 mVar R ⁡ ∅
7 eqid ⊢ 1 𝑜 mVar R = 1 𝑜 mVar R
8 1on ⊢ 1 𝑜 ∈ On
9 8 a1i ⊢ φ → 1 𝑜 ∈ On
10 eqid ⊢ 1 𝑜 mPoly H = 1 𝑜 mPoly H
11 4 5 ply1bas ⊢ B = Base 1 𝑜 mPoly H
12 7 9 2 3 10 11 subrgmvrf ⊢ φ → 1 𝑜 mVar R : 1 𝑜 ⟶ B
13 0lt1o ⊢ ∅ ∈ 1 𝑜
14 ffvelcdm ⊢ 1 𝑜 mVar R : 1 𝑜 ⟶ B ∧ ∅ ∈ 1 𝑜 → 1 𝑜 mVar R ⁡ ∅ ∈ B
15 12 13 14 sylancl ⊢ φ → 1 𝑜 mVar R ⁡ ∅ ∈ B
16 6 15 eqeltrid ⊢ φ → X ∈ B