Metamath Proof Explorer

Theorem subrgmvrf

Description: The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses subrgmvr.v ⊢ V = I mVar R
subrgmvr.i ⊢ φ → I ∈ W
subrgmvr.r ⊢ φ → T ∈ SubRing ⁡ R
subrgmvr.h ⊢ H = R ↾ 𝑠 T
subrgmvrf.u ⊢ U = I mPoly H
subrgmvrf.b ⊢ B = Base U
Assertion subrgmvrf ⊢ φ → V : I ⟶ B

Proof

Step Hyp Ref Expression
1 subrgmvr.v ⊢ V = I mVar R
2 subrgmvr.i ⊢ φ → I ∈ W
3 subrgmvr.r ⊢ φ → T ∈ SubRing ⁡ R
4 subrgmvr.h ⊢ H = R ↾ 𝑠 T
5 subrgmvrf.u ⊢ U = I mPoly H
6 subrgmvrf.b ⊢ B = Base U
7 eqid ⊢ I mPwSer R = I mPwSer R
8 eqid ⊢ Base I mPwSer R = Base I mPwSer R
9 subrgrcl ⊢ T ∈ SubRing ⁡ R → R ∈ Ring
10 3 9 syl ⊢ φ → R ∈ Ring
11 7 1 8 2 10 mvrf ⊢ φ → V : I ⟶ Base I mPwSer R
12 11 ffnd ⊢ φ → V Fn I
13 1 2 3 4 subrgmvr ⊢ φ → V = I mVar H
14 13 fveq1d ⊢ φ → V ⁡ x = I mVar H ⁡ x
15 14 adantr ⊢ φ ∧ x ∈ I → V ⁡ x = I mVar H ⁡ x
16 eqid ⊢ I mVar H = I mVar H
17 2 adantr ⊢ φ ∧ x ∈ I → I ∈ W
18 4 subrgring ⊢ T ∈ SubRing ⁡ R → H ∈ Ring
19 3 18 syl ⊢ φ → H ∈ Ring
20 19 adantr ⊢ φ ∧ x ∈ I → H ∈ Ring
21 simpr ⊢ φ ∧ x ∈ I → x ∈ I
22 5 16 6 17 20 21 mvrcl ⊢ φ ∧ x ∈ I → I mVar H ⁡ x ∈ B
23 15 22 eqeltrd ⊢ φ ∧ x ∈ I → V ⁡ x ∈ B
24 23 ralrimiva ⊢ φ → ∀ x ∈ I V ⁡ x ∈ B
25 ffnfv ⊢ V : I ⟶ B ↔ V Fn I ∧ ∀ x ∈ I V ⁡ x ∈ B
26 12 24 25 sylanbrc ⊢ φ → V : I ⟶ B