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

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 ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
selvcllemh.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvcllemh.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
selvcllemh.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
selvcllemh.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
selvcllemh.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
selvcllemh.s ⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
selvcllemh.x ⊢ 𝑋 = ( 𝑇 ↑s ( 𝐵 ↑m 𝐼 ) )
selvcllemh.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
selvcllemh.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
selvcllemh.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
selvcllemh.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion selvcllemh ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )

Proof

Step Hyp Ref Expression
1 selvcllemh.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
2 selvcllemh.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
3 selvcllemh.c ⊢ 𝐶 = ( algSc ‘ 𝑇 )
4 selvcllemh.d ⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
5 selvcllemh.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑇 ) ‘ ran 𝐷 )
6 selvcllemh.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
7 selvcllemh.s ⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
8 selvcllemh.x ⊢ 𝑋 = ( 𝑇 ↑s ( 𝐵 ↑m 𝐼 ) )
9 selvcllemh.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
10 selvcllemh.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11 selvcllemh.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
12 selvcllemh.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
13 10 12 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
14 10 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
15 1 mplcrng ⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ CRing )
16 14 11 15 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ CRing )
17 2 mplcrng ⊢ ( ( 𝐽 ∈ V ∧ 𝑈 ∈ CRing ) → 𝑇 ∈ CRing )
18 13 16 17 syl2anc ⊢ ( 𝜑 → 𝑇 ∈ CRing )
19 1 2 3 4 14 13 11 selvcllem3 ⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
20 5 6 7 8 9 evlsrhm ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑇 ∈ CRing ∧ ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) ) → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )
21 10 18 19 20 syl3anc ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑊 RingHom 𝑋 ) )