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

Metamath Proof Explorer

Theorem selvcllem3

Description: The third argument passed to evalSub is in the domain. (Contributed by SN, 15-Dec-2023)

Ref Expression
Hypotheses selvcllem2.u ⊢ U = I mPoly R
selvcllem2.t ⊢ T = J mPoly U
selvcllem2.c ⊢ C = algSc ⁡ T
selvcllem2.d ⊢ D = C ∘ algSc ⁡ U
selvcllem2.i ⊢ φ → I ∈ V
selvcllem2.j ⊢ φ → J ∈ W
selvcllem2.r ⊢ φ → R ∈ CRing
Assertion selvcllem3 ⊢ φ → ran ⁡ D ∈ SubRing ⁡ T

Proof

Step Hyp Ref Expression
1 selvcllem2.u ⊢ U = I mPoly R
2 selvcllem2.t ⊢ T = J mPoly U
3 selvcllem2.c ⊢ C = algSc ⁡ T
4 selvcllem2.d ⊢ D = C ∘ algSc ⁡ U
5 selvcllem2.i ⊢ φ → I ∈ V
6 selvcllem2.j ⊢ φ → J ∈ W
7 selvcllem2.r ⊢ φ → R ∈ CRing
8 1 2 3 4 5 6 7 selvcllem2 ⊢ φ → D ∈ R RingHom T
9 rnrhmsubrg ⊢ D ∈ R RingHom T → ran ⁡ D ∈ SubRing ⁡ T
10 8 9 syl ⊢ φ → ran ⁡ D ∈ SubRing ⁡ T