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

Metamath Proof Explorer

Theorem selvcllem4

Description: The fourth argument passed to evalSub is in the domain (a polynomial in ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ). (Contributed by SN, 5-Nov-2023)

Ref Expression
Hypotheses selvcllem4.p ⊢ P = I mPoly R
selvcllem4.b ⊢ B = Base P
selvcllem4.u ⊢ U = I ∖ J mPoly R
selvcllem4.t ⊢ T = J mPoly U
selvcllem4.c ⊢ C = algSc ⁡ T
selvcllem4.d ⊢ D = C ∘ algSc ⁡ U
selvcllem4.s ⊢ S = T ↾ 𝑠 ran ⁡ D
selvcllem4.w ⊢ W = I mPoly S
selvcllem4.x ⊢ X = Base W
selvcllem4.r ⊢ φ → R ∈ CRing
selvcllem4.j ⊢ φ → J ⊆ I
selvcllem4.f ⊢ φ → F ∈ B
Assertion selvcllem4 ⊢ φ → D ∘ F ∈ X

Proof

Step Hyp Ref Expression
1 selvcllem4.p ⊢ P = I mPoly R
2 selvcllem4.b ⊢ B = Base P
3 selvcllem4.u ⊢ U = I ∖ J mPoly R
4 selvcllem4.t ⊢ T = J mPoly U
5 selvcllem4.c ⊢ C = algSc ⁡ T
6 selvcllem4.d ⊢ D = C ∘ algSc ⁡ U
7 selvcllem4.s ⊢ S = T ↾ 𝑠 ran ⁡ D
8 selvcllem4.w ⊢ W = I mPoly S
9 selvcllem4.x ⊢ X = Base W
10 selvcllem4.r ⊢ φ → R ∈ CRing
11 selvcllem4.j ⊢ φ → J ⊆ I
12 selvcllem4.f ⊢ φ → F ∈ B
13 1 2 mplrcl ⊢ F ∈ B → I ∈ V
14 12 13 syl ⊢ φ → I ∈ V
15 14 difexd ⊢ φ → I ∖ J ∈ V
16 14 11 ssexd ⊢ φ → J ∈ V
17 3 4 5 6 15 16 10 selvcllem2 ⊢ φ → D ∈ R RingHom T
18 3 4 5 6 15 16 10 selvcllem3 ⊢ φ → ran ⁡ D ∈ SubRing ⁡ T
19 ssidd ⊢ φ → ran ⁡ D ⊆ ran ⁡ D
20 7 resrhm2b ⊢ ran ⁡ D ∈ SubRing ⁡ T ∧ ran ⁡ D ⊆ ran ⁡ D → D ∈ R RingHom T ↔ D ∈ R RingHom S
21 18 19 20 syl2anc ⊢ φ → D ∈ R RingHom T ↔ D ∈ R RingHom S
22 17 21 mpbid ⊢ φ → D ∈ R RingHom S
23 rhmghm ⊢ D ∈ R RingHom S → D ∈ R GrpHom S
24 ghmmhm ⊢ D ∈ R GrpHom S → D ∈ R MndHom S
25 22 23 24 3syl ⊢ φ → D ∈ R MndHom S
26 1 8 2 9 25 12 mhmcompl ⊢ φ → D ∘ F ∈ X