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 )