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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	rhmply1vr1.q	⊢ 𝑄 = ( Poly₁ ‘ 𝑆 )
	rhmply1vr1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	rhmply1vr1.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
	rhmply1vr1.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	rhmply1vr1.y	⊢ 𝑌 = ( var₁ ‘ 𝑆 )
	rhmply1vr1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion	rhmply1vr1	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		rhmply1vr1.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		rhmply1vr1.q	⊢ 𝑄 = ( Poly₁ ‘ 𝑆 )
3		rhmply1vr1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		rhmply1vr1.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
5		rhmply1vr1.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
6		rhmply1vr1.y	⊢ 𝑌 = ( var₁ ‘ 𝑆 )
7		rhmply1vr1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
8		coeq2	⊢ ( 𝑝 = 𝑋 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑋 ) )
9		rhmrcl1	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
10	7 9	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
11	5 1 3	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
12	10 11	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13	5	fvexi	⊢ 𝑋 ∈ V
14	13	a1i	⊢ ( 𝜑 → 𝑋 ∈ V )
15	7 14	coexd	⊢ ( 𝜑 → ( 𝐻 ∘ 𝑋 ) ∈ V )
16	4 8 12 15	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( 𝐻 ∘ 𝑋 ) )
17		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
19	17 18	rhmf	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
20	7 19	syl	⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
21		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
22	17 21	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
23	10 22	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
24		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
25	17 24	ring0cl	⊢ ( 𝑅 ∈ Ring → ( 0_g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
26	10 25	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27	23 26	ifcld	⊢ ( 𝜑 → if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ) → if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
29	20 28	cofmpt	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ) )
30		fvif	⊢ ( 𝐻 ‘ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) = if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 𝐻 ‘ ( 1_r ‘ 𝑅 ) ) , ( 𝐻 ‘ ( 0_g ‘ 𝑅 ) ) )
31		eqid	⊢ ( 1_r ‘ 𝑆 ) = ( 1_r ‘ 𝑆 )
32	21 31	rhm1	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐻 ‘ ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑆 ) )
33	7 32	syl	⊢ ( 𝜑 → ( 𝐻 ‘ ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑆 ) )
34		rhmghm	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
35		eqid	⊢ ( 0_g ‘ 𝑆 ) = ( 0_g ‘ 𝑆 )
36	24 35	ghmid	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐻 ‘ ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑆 ) )
37	7 34 36	3syl	⊢ ( 𝜑 → ( 𝐻 ‘ ( 0_g ‘ 𝑅 ) ) = ( 0_g ‘ 𝑆 ) )
38	33 37	ifeq12d	⊢ ( 𝜑 → if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 𝐻 ‘ ( 1_r ‘ 𝑅 ) ) , ( 𝐻 ‘ ( 0_g ‘ 𝑅 ) ) ) = if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑆 ) , ( 0_g ‘ 𝑆 ) ) )
39	30 38	eqtrid	⊢ ( 𝜑 → ( 𝐻 ‘ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) = if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑆 ) , ( 0_g ‘ 𝑆 ) ) )
40	39	mpteq2dv	⊢ ( 𝜑 → ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑆 ) , ( 0_g ‘ 𝑆 ) ) ) )
41	29 40	eqtrd	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑆 ) , ( 0_g ‘ 𝑆 ) ) ) )
42		eqid	⊢ ( 1_o mVar 𝑅 ) = ( 1_o mVar 𝑅 )
43		eqid	⊢ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
44		1oex	⊢ 1_o ∈ V
45	44	a1i	⊢ ( 𝜑 → 1_o ∈ V )
46		0lt1o	⊢ ∅ ∈ 1_o
47	46	a1i	⊢ ( 𝜑 → ∅ ∈ 1_o )
48	42 43 24 21 45 10 47	mvrval	⊢ ( 𝜑 → ( ( 1_o mVar 𝑅 ) ‘ ∅ ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) )
49	48	coeq2d	⊢ ( 𝜑 → ( 𝐻 ∘ ( ( 1_o mVar 𝑅 ) ‘ ∅ ) ) = ( 𝐻 ∘ ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑅 ) , ( 0_g ‘ 𝑅 ) ) ) ) )
50		eqid	⊢ ( 1_o mVar 𝑆 ) = ( 1_o mVar 𝑆 )
51		rhmrcl2	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
52	7 51	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
53	50 43 35 31 45 52 47	mvrval	⊢ ( 𝜑 → ( ( 1_o mVar 𝑆 ) ‘ ∅ ) = ( 𝑓 ∈ { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑓 = ( 𝑦 ∈ 1_o ↦ if ( 𝑦 = ∅ , 1 , 0 ) ) , ( 1_r ‘ 𝑆 ) , ( 0_g ‘ 𝑆 ) ) ) )
54	41 49 53	3eqtr4d	⊢ ( 𝜑 → ( 𝐻 ∘ ( ( 1_o mVar 𝑅 ) ‘ ∅ ) ) = ( ( 1_o mVar 𝑆 ) ‘ ∅ ) )
55	5	vr1val	⊢ 𝑋 = ( ( 1_o mVar 𝑅 ) ‘ ∅ )
56	55	coeq2i	⊢ ( 𝐻 ∘ 𝑋 ) = ( 𝐻 ∘ ( ( 1_o mVar 𝑅 ) ‘ ∅ ) )
57	6	vr1val	⊢ 𝑌 = ( ( 1_o mVar 𝑆 ) ‘ ∅ )
58	54 56 57	3eqtr4g	⊢ ( 𝜑 → ( 𝐻 ∘ 𝑋 ) = 𝑌 )
59	16 58	eqtrd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )

Metamath Proof Explorer

Theorem rhmply1vr1

Proof