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 = Poly 1 R
rhmply1vr1.q Q = Poly 1 S
rhmply1vr1.b B = Base P
rhmply1vr1.f F = p B H p
rhmply1vr1.x X = var 1 R
rhmply1vr1.y Y = var 1 S
rhmply1vr1.h φ H R RingHom S
Assertion rhmply1vr1 φ F X = Y

Proof

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