Metamath Proof Explorer

Theorem rhmply1vr1

Description: A ring homomorphism between two univariate polynomial algebras sends one variable to the other. (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses rhmply1vr1.p 
|- P = ( Poly1 ` R )
rhmply1vr1.q 
|- Q = ( Poly1 ` S )
rhmply1vr1.b 
|- B = ( Base ` P )
rhmply1vr1.f 
|- F = ( p e. B |-> ( H o. p ) )
rhmply1vr1.x 
|- X = ( var1 ` R )
rhmply1vr1.y 
|- Y = ( var1 ` S )
rhmply1vr1.h 
|- ( ph -> H e. ( R RingHom S ) )
Assertion rhmply1vr1 
|- ( ph -> ( F ` X ) = Y )

Proof

Step Hyp Ref Expression
1 rhmply1vr1.p 
 |-  P = ( Poly1 ` R )
2 rhmply1vr1.q 
 |-  Q = ( Poly1 ` S )
3 rhmply1vr1.b 
 |-  B = ( Base ` P )
4 rhmply1vr1.f 
 |-  F = ( p e. B |-> ( H o. p ) )
5 rhmply1vr1.x 
 |-  X = ( var1 ` R )
6 rhmply1vr1.y 
 |-  Y = ( var1 ` S )
7 rhmply1vr1.h 
 |-  ( ph -> H e. ( R RingHom S ) )
8 coeq2 
 |-  ( p = X -> ( H o. p ) = ( H o. X ) )
9 rhmrcl1 
 |-  ( H e. ( R RingHom S ) -> R e. Ring )
10 7 9 syl 
 |-  ( ph -> R e. Ring )
11 5 1 3 vr1cl 
 |-  ( R e. Ring -> X e. B )
12 10 11 syl 
 |-  ( ph -> X e. B )
13 5 fvexi 
 |-  X e. _V
14 13 a1i 
 |-  ( ph -> X e. _V )
15 7 14 coexd 
 |-  ( ph -> ( H o. X ) e. _V )
16 4 8 12 15 fvmptd3 
 |-  ( ph -> ( F ` X ) = ( H o. X ) )
17 eqid 
 |-  ( Base ` R ) = ( Base ` R )
18 eqid 
 |-  ( Base ` S ) = ( Base ` S )
19 17 18 rhmf 
 |-  ( H e. ( R RingHom S ) -> H : ( Base ` R ) --> ( Base ` S ) )
20 7 19 syl 
 |-  ( ph -> H : ( Base ` R ) --> ( Base ` S ) )
21 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
22 17 21 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
23 10 22 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
24 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
25 17 24 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
26 10 25 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
27 23 26 ifcld 
 |-  ( ph -> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
28 27 adantr 
 |-  ( ( ph /\ f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } ) -> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )
29 20 28 cofmpt 
 |-  ( ph -> ( H o. ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
30 fvif 
 |-  ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( H ` ( 1r ` R ) ) , ( H ` ( 0g ` R ) ) )
31 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
32 21 31 rhm1 
 |-  ( H e. ( R RingHom S ) -> ( H ` ( 1r ` R ) ) = ( 1r ` S ) )
33 7 32 syl 
 |-  ( ph -> ( H ` ( 1r ` R ) ) = ( 1r ` S ) )
34 rhmghm 
 |-  ( H e. ( R RingHom S ) -> H e. ( R GrpHom S ) )
35 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
36 24 35 ghmid 
 |-  ( H e. ( R GrpHom S ) -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) )
37 7 34 36 3syl 
 |-  ( ph -> ( H ` ( 0g ` R ) ) = ( 0g ` S ) )
38 33 37 ifeq12d 
 |-  ( ph -> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( H ` ( 1r ` R ) ) , ( H ` ( 0g ` R ) ) ) = if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) )
39 30 38 eqtrid 
 |-  ( ph -> ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) = if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) )
40 39 mpteq2dv 
 |-  ( ph -> ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> ( H ` if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) )
41 29 40 eqtrd 
 |-  ( ph -> ( H o. ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) )
42 eqid 
 |-  ( 1o mVar R ) = ( 1o mVar R )
43 eqid 
 |-  { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
44 1oex 
 |-  1o e. _V
45 44 a1i 
 |-  ( ph -> 1o e. _V )
46 0lt1o 
 |-  (/) e. 1o
47 46 a1i 
 |-  ( ph -> (/) e. 1o )
48 42 43 24 21 45 10 47 mvrval 
 |-  ( ph -> ( ( 1o mVar R ) ` (/) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
49 48 coeq2d 
 |-  ( ph -> ( H o. ( ( 1o mVar R ) ` (/) ) ) = ( H o. ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) )
50 eqid 
 |-  ( 1o mVar S ) = ( 1o mVar S )
51 rhmrcl2 
 |-  ( H e. ( R RingHom S ) -> S e. Ring )
52 7 51 syl 
 |-  ( ph -> S e. Ring )
53 50 43 35 31 45 52 47 mvrval 
 |-  ( ph -> ( ( 1o mVar S ) ` (/) ) = ( f e. { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin } |-> if ( f = ( y e. 1o |-> if ( y = (/) , 1 , 0 ) ) , ( 1r ` S ) , ( 0g ` S ) ) ) )
54 41 49 53 3eqtr4d 
 |-  ( ph -> ( H o. ( ( 1o mVar R ) ` (/) ) ) = ( ( 1o mVar S ) ` (/) ) )
55 5 vr1val 
 |-  X = ( ( 1o mVar R ) ` (/) )
56 55 coeq2i 
 |-  ( H o. X ) = ( H o. ( ( 1o mVar R ) ` (/) ) )
57 6 vr1val 
 |-  Y = ( ( 1o mVar S ) ` (/) )
58 54 56 57 3eqtr4g 
 |-  ( ph -> ( H o. X ) = Y )
59 16 58 eqtrd 
 |-  ( ph -> ( F ` X ) = Y )