Metamath Proof Explorer

Theorem selvply1rhm

Description: Build a ring homomorphism H between the multivariate polynomials P with variables in I and the univariate polynomials Q in a single variable X element of I . (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses selvply1rhm.1 
|- B = ( Base ` P )
selvply1rhm.2 
|- P = ( I mPoly R )
selvply1rhm.3 
|- U = ( ( I \ { X } ) mPoly R )
selvply1rhm.4 
|- Q = ( Poly1 ` U )
selvply1rhm.5 
|- H = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) )
selvply1rhm.6 
|- ( ph -> I e. V )
selvply1rhm.7 
|- ( ph -> X e. I )
selvply1rhm.8 
|- ( ph -> R e. CRing )
Assertion selvply1rhm 
|- ( ph -> H e. ( P RingHom Q ) )

Proof

Step Hyp Ref Expression
1 selvply1rhm.1 
 |-  B = ( Base ` P )
2 selvply1rhm.2 
 |-  P = ( I mPoly R )
3 selvply1rhm.3 
 |-  U = ( ( I \ { X } ) mPoly R )
4 selvply1rhm.4 
 |-  Q = ( Poly1 ` U )
5 selvply1rhm.5 
 |-  H = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) )
6 selvply1rhm.6 
 |-  ( ph -> I e. V )
7 selvply1rhm.7 
 |-  ( ph -> X e. I )
8 selvply1rhm.8 
 |-  ( ph -> R e. CRing )
9 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
10 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
11 eqid 
 |-  ( .r ` P ) = ( .r ` P )
12 eqid 
 |-  ( .r ` Q ) = ( .r ` Q )
13 8 crngringd 
 |-  ( ph -> R e. Ring )
14 2 6 13 mplringd 
 |-  ( ph -> P e. Ring )
15 6 difexd 
 |-  ( ph -> ( I \ { X } ) e. _V )
16 3 15 13 mplringd 
 |-  ( ph -> U e. Ring )
17 4 ply1ring 
 |-  ( U e. Ring -> Q e. Ring )
18 16 17 syl 
 |-  ( ph -> Q e. Ring )
19 1 2 3 4 5 6 7 8 selvply1rhmlem2 
 |-  ( ph -> ( H ` ( 1r ` P ) ) = ( 1r ` Q ) )
20 eqid 
 |-  ( Base ` ( { X } mPoly U ) ) = ( Base ` ( { X } mPoly U ) )
21 eqid 
 |-  ( { X } mPoly U ) = ( { X } mPoly U )
22 eqid 
 |-  ( .r ` ( { X } mPoly U ) ) = ( .r ` ( { X } mPoly U ) )
23 fveq1 
 |-  ( p = q -> ( p ` { <. X , ( r ` (/) ) >. } ) = ( q ` { <. X , ( r ` (/) ) >. } ) )
24 23 mpteq2dv 
 |-  ( p = q -> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) = ( r e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( r ` (/) ) >. } ) ) )
25 24 cbvmptv 
 |-  ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( r ` (/) ) >. } ) ) )
26 fveq1 
 |-  ( r = s -> ( r ` (/) ) = ( s ` (/) ) )
27 26 opeq2d 
 |-  ( r = s -> <. X , ( r ` (/) ) >. = <. X , ( s ` (/) ) >. )
28 27 sneqd 
 |-  ( r = s -> { <. X , ( r ` (/) ) >. } = { <. X , ( s ` (/) ) >. } )
29 28 fveq2d 
 |-  ( r = s -> ( q ` { <. X , ( r ` (/) ) >. } ) = ( q ` { <. X , ( s ` (/) ) >. } ) )
30 29 cbvmptv 
 |-  ( r e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( r ` (/) ) >. } ) ) = ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) )
31 30 mpteq2i 
 |-  ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( r ` (/) ) >. } ) ) ) = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) ) )
32 25 31 eqtri 
 |-  ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) ) )
33 7 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> X e. I )
34 16 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> U e. Ring )
35 8 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> R e. CRing )
36 7 snssd 
 |-  ( ph -> { X } C_ I )
37 36 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> { X } C_ I )
38 simplr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> g e. B )
39 2 1 3 21 20 35 37 38 selvcl 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( ( ( I selectVars R ) ` { X } ) ` g ) e. ( Base ` ( { X } mPoly U ) ) )
40 simpr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> h e. B )
41 2 1 3 21 20 35 37 40 selvcl 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( ( ( I selectVars R ) ` { X } ) ` h ) e. ( Base ` ( { X } mPoly U ) ) )
42 20 21 22 12 4 32 33 34 39 41 selvply1rhmlemb 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( ( I selectVars R ) ` { X } ) ` g ) ( .r ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` h ) ) ) = ( ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` g ) ) ( .r ` Q ) ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` h ) ) ) )
43 6 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> I e. V )
44 14 ad2antrr 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> P e. Ring )
45 1 11 44 38 40 ringcld 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( g ( .r ` P ) h ) e. B )
46 1 2 3 4 5 43 33 35 45 25 selvply1rhmlem5 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( H ` ( g ( .r ` P ) h ) ) = ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` ( g ( .r ` P ) h ) ) ) )
47 2 1 11 3 21 22 43 35 37 38 40 selvmul 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( ( ( I selectVars R ) ` { X } ) ` ( g ( .r ` P ) h ) ) = ( ( ( ( I selectVars R ) ` { X } ) ` g ) ( .r ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` h ) ) )
48 47 fveq2d 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` ( g ( .r ` P ) h ) ) ) = ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( ( I selectVars R ) ` { X } ) ` g ) ( .r ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` h ) ) ) )
49 46 48 eqtrd 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( H ` ( g ( .r ` P ) h ) ) = ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( ( I selectVars R ) ` { X } ) ` g ) ( .r ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` h ) ) ) )
50 1 2 3 4 5 43 33 35 38 25 selvply1rhmlem5 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( H ` g ) = ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` g ) ) )
51 1 2 3 4 5 43 33 35 40 25 selvply1rhmlem5 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( H ` h ) = ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` h ) ) )
52 50 51 oveq12d 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( ( H ` g ) ( .r ` Q ) ( H ` h ) ) = ( ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` g ) ) ( .r ` Q ) ( ( p e. ( Base ` ( { X } mPoly U ) ) |-> ( r e. ( NN0 ^m 1o ) |-> ( p ` { <. X , ( r ` (/) ) >. } ) ) ) ` ( ( ( I selectVars R ) ` { X } ) ` h ) ) ) )
53 42 49 52 3eqtr4d 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( H ` ( g ( .r ` P ) h ) ) = ( ( H ` g ) ( .r ` Q ) ( H ` h ) ) )
54 53 anasss 
 |-  ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( H ` ( g ( .r ` P ) h ) ) = ( ( H ` g ) ( .r ` Q ) ( H ` h ) ) )
55 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
56 eqid 
 |-  ( +g ` P ) = ( +g ` P )
57 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
58 1 2 3 4 5 6 7 8 selvply1rhmlem1 
 |-  ( ph -> H : B --> ( Base ` Q ) )
59 1 2 3 4 5 43 33 35 38 40 selvply1rhmlem4 
 |-  ( ( ( ph /\ g e. B ) /\ h e. B ) -> ( H ` ( g ( +g ` P ) h ) ) = ( ( H ` g ) ( +g ` Q ) ( H ` h ) ) )
60 59 anasss 
 |-  ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( H ` ( g ( +g ` P ) h ) ) = ( ( H ` g ) ( +g ` Q ) ( H ` h ) ) )
61 1 9 10 11 12 14 18 19 54 55 56 57 58 60 isrhmd 
 |-  ( ph -> H e. ( P RingHom Q ) )