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 
|- U = ( ( I \ J ) mPoly R )
selvcllemh.t 
|- T = ( J mPoly U )
selvcllemh.c 
|- C = ( algSc ` T )
selvcllemh.d 
|- D = ( C o. ( algSc ` U ) )
selvcllemh.q 
|- Q = ( ( I evalSub T ) ` ran D )
selvcllemh.w 
|- W = ( I mPoly S )
selvcllemh.s 
|- S = ( T |`s ran D )
selvcllemh.x 
|- X = ( T ^s ( B ^m I ) )
selvcllemh.b 
|- B = ( Base ` T )
selvcllemh.i 
|- ( ph -> I e. V )
selvcllemh.r 
|- ( ph -> R e. CRing )
selvcllemh.j 
|- ( ph -> J C_ I )
Assertion selvcllemh 
|- ( ph -> Q e. ( 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 o. ( algSc ` U ) )
5 selvcllemh.q 
 |-  Q = ( ( I evalSub T ) ` ran D )
6 selvcllemh.w 
 |-  W = ( I mPoly S )
7 selvcllemh.s 
 |-  S = ( T |`s ran D )
8 selvcllemh.x 
 |-  X = ( T ^s ( B ^m I ) )
9 selvcllemh.b 
 |-  B = ( Base ` T )
10 selvcllemh.i 
 |-  ( ph -> I e. V )
11 selvcllemh.r 
 |-  ( ph -> R e. CRing )
12 selvcllemh.j 
 |-  ( ph -> J C_ I )
13 10 12 ssexd 
 |-  ( ph -> J e. _V )
14 10 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
15 1 mplcrng 
 |-  ( ( ( I \ J ) e. _V /\ R e. CRing ) -> U e. CRing )
16 14 11 15 syl2anc 
 |-  ( ph -> U e. CRing )
17 2 mplcrng 
 |-  ( ( J e. _V /\ U e. CRing ) -> T e. CRing )
18 13 16 17 syl2anc 
 |-  ( ph -> T e. CRing )
19 1 2 3 4 14 13 11 selvcllem3 
 |-  ( ph -> ran D e. ( SubRing ` T ) )
20 5 6 7 8 9 evlsrhm 
 |-  ( ( I e. V /\ T e. CRing /\ ran D e. ( SubRing ` T ) ) -> Q e. ( W RingHom X ) )
21 10 18 19 20 syl3anc 
 |-  ( ph -> Q e. ( W RingHom X ) )