Metamath Proof Explorer

Theorem selvcllemh

Description: Apply the third argument ( selvcllem3 ) to show that Q is a (ring) homomorphism. (Contributed by SN, 5-Nov-2023)

Ref Expression
Hypotheses selvcllemh.u ⊢ U = I ∖ J mPoly R
selvcllemh.t ⊢ T = J mPoly U
selvcllemh.c ⊢ C = algSc ⁡ T
selvcllemh.d ⊢ D = C ∘ algSc ⁡ U
selvcllemh.q ⊢ Q = I evalSub T ⁡ ran ⁡ D
selvcllemh.w ⊢ W = I mPoly S
selvcllemh.s ⊢ S = T ↾ 𝑠 ran ⁡ D
selvcllemh.x ⊢ X = T ↑ 𝑠 B I
selvcllemh.b ⊢ B = Base T
selvcllemh.i ⊢ φ → I ∈ V
selvcllemh.r ⊢ φ → R ∈ CRing
selvcllemh.j ⊢ φ → J ⊆ I
Assertion selvcllemh ⊢ φ → Q ∈ W RingHom X

Proof

Step Hyp Ref Expression
1 selvcllemh.u ⊢ U = I ∖ J mPoly R
2 selvcllemh.t ⊢ T = J mPoly U
3 selvcllemh.c ⊢ C = algSc ⁡ T
4 selvcllemh.d ⊢ D = C ∘ algSc ⁡ U
5 selvcllemh.q ⊢ Q = I evalSub T ⁡ ran ⁡ D
6 selvcllemh.w ⊢ W = I mPoly S
7 selvcllemh.s ⊢ S = T ↾ 𝑠 ran ⁡ D
8 selvcllemh.x ⊢ X = T ↑ 𝑠 B I
9 selvcllemh.b ⊢ B = Base T
10 selvcllemh.i ⊢ φ → I ∈ V
11 selvcllemh.r ⊢ φ → R ∈ CRing
12 selvcllemh.j ⊢ φ → J ⊆ I
13 10 12 ssexd ⊢ φ → J ∈ V
14 10 difexd ⊢ φ → I ∖ J ∈ V
15 1 mplcrng ⊢ I ∖ J ∈ V ∧ R ∈ CRing → U ∈ CRing
16 14 11 15 syl2anc ⊢ φ → U ∈ CRing
17 2 mplcrng ⊢ J ∈ V ∧ U ∈ CRing → T ∈ CRing
18 13 16 17 syl2anc ⊢ φ → T ∈ CRing
19 1 2 3 4 14 13 11 selvcllem3 ⊢ φ → ran ⁡ D ∈ SubRing ⁡ T
20 5 6 7 8 9 evlsrhm ⊢ I ∈ V ∧ T ∈ CRing ∧ ran ⁡ D ∈ SubRing ⁡ T → Q ∈ W RingHom X
21 10 18 19 20 syl3anc ⊢ φ → Q ∈ W RingHom X