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	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
	selvply1rhm.4	⊢ 𝑄 = ( Poly₁ ‘ 𝑈 )
	selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
	selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	selvply1rhm	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
2		selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
4		selvply1rhm.4	⊢ 𝑄 = ( Poly₁ ‘ 𝑈 )
5		selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
6		selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8		selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
9		eqid	⊢ ( 1_r ‘ 𝑃 ) = ( 1_r ‘ 𝑃 )
10		eqid	⊢ ( 1_r ‘ 𝑄 ) = ( 1_r ‘ 𝑄 )
11		eqid	⊢ ( ._r ‘ 𝑃 ) = ( ._r ‘ 𝑃 )
12		eqid	⊢ ( ._r ‘ 𝑄 ) = ( ._r ‘ 𝑄 )
13	8	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
14	2 6 13	mplringd	⊢ ( 𝜑 → 𝑃 ∈ Ring )
15	6	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ∈ V )
16	3 15 13	mplringd	⊢ ( 𝜑 → 𝑈 ∈ Ring )
17	4	ply1ring	⊢ ( 𝑈 ∈ Ring → 𝑄 ∈ Ring )
18	16 17	syl	⊢ ( 𝜑 → 𝑄 ∈ Ring )
19	1 2 3 4 5 6 7 8	selvply1rhmlem2	⊢ ( 𝜑 → ( 𝐻 ‘ ( 1_r ‘ 𝑃 ) ) = ( 1_r ‘ 𝑄 ) )
20		eqid	⊢ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) )
21		eqid	⊢ ( { 𝑋 } mPoly 𝑈 ) = ( { 𝑋 } mPoly 𝑈 )
22		eqid	⊢ ( ._r ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( ._r ‘ ( { 𝑋 } mPoly 𝑈 ) )
23		fveq1	⊢ ( 𝑝 = 𝑞 → ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) = ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) )
24	23	mpteq2dv	⊢ ( 𝑝 = 𝑞 → ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) = ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) )
25	24	cbvmptv	⊢ ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) )
26		fveq1	⊢ ( 𝑟 = 𝑠 → ( 𝑟 ‘ ∅ ) = ( 𝑠 ‘ ∅ ) )
27	26	opeq2d	⊢ ( 𝑟 = 𝑠 → ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ )
28	27	sneqd	⊢ ( 𝑟 = 𝑠 → { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } )
29	28	fveq2d	⊢ ( 𝑟 = 𝑠 → ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) = ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) )
30	29	cbvmptv	⊢ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) = ( 𝑠 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) )
31	30	mpteq2i	⊢ ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑠 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) ) )
32	25 31	eqtri	⊢ ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑠 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) ) )
33	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → 𝑋 ∈ 𝐼 )
34	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → 𝑈 ∈ Ring )
35	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → 𝑅 ∈ CRing )
36	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
37	36	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → { 𝑋 } ⊆ 𝐼 )
38		simplr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → 𝑔 ∈ 𝐵 )
39	2 1 3 21 20 35 37 38	selvcl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ℎ ∈ 𝐵 )
41	2 1 3 21 20 35 37 40	selvcl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) )
42	20 21 22 12 4 32 33 34 39 41	selvply1rhmlemb	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ( ._r ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) ) = ( ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ) ( ._r ‘ 𝑄 ) ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) ) )
43	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
44	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → 𝑃 ∈ Ring )
45	1 11 44 38 40	ringcld	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ∈ 𝐵 )
46	1 2 3 4 5 43 33 35 45 25	selvply1rhmlem5	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝐻 ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) = ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) ) )
47	2 1 11 3 21 22 43 35 37 38 40	selvmul	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ( ._r ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) )
48	47	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) ) = ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ( ._r ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) ) )
49	46 48	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝐻 ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) = ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ( ._r ‘ ( { 𝑋 } mPoly 𝑈 ) ) ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) ) )
50	1 2 3 4 5 43 33 35 38 25	selvply1rhmlem5	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝐻 ‘ 𝑔 ) = ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ) )
51	1 2 3 4 5 43 33 35 40 25	selvply1rhmlem5	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝐻 ‘ ℎ ) = ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) )
52	50 51	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑔 ) ( ._r ‘ 𝑄 ) ( 𝐻 ‘ ℎ ) ) = ( ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑔 ) ) ( ._r ‘ 𝑄 ) ( ( 𝑝 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑟 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( 𝑝 ‘ { ⟨ 𝑋 , ( 𝑟 ‘ ∅ ) ⟩ } ) ) ) ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ℎ ) ) ) )
53	42 49 52	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝐻 ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) = ( ( 𝐻 ‘ 𝑔 ) ( ._r ‘ 𝑄 ) ( 𝐻 ‘ ℎ ) ) )
54	53	anasss	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑔 ( ._r ‘ 𝑃 ) ℎ ) ) = ( ( 𝐻 ‘ 𝑔 ) ( ._r ‘ 𝑄 ) ( 𝐻 ‘ ℎ ) ) )
55		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
56		eqid	⊢ ( +_g ‘ 𝑃 ) = ( +_g ‘ 𝑃 )
57		eqid	⊢ ( +_g ‘ 𝑄 ) = ( +_g ‘ 𝑄 )
58	1 2 3 4 5 6 7 8	selvply1rhmlem1	⊢ ( 𝜑 → 𝐻 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
59	1 2 3 4 5 43 33 35 38 40	selvply1rhmlem4	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐵 ) ∧ ℎ ∈ 𝐵 ) → ( 𝐻 ‘ ( 𝑔 ( +_g ‘ 𝑃 ) ℎ ) ) = ( ( 𝐻 ‘ 𝑔 ) ( +_g ‘ 𝑄 ) ( 𝐻 ‘ ℎ ) ) )
60	59	anasss	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( 𝐻 ‘ ( 𝑔 ( +_g ‘ 𝑃 ) ℎ ) ) = ( ( 𝐻 ‘ 𝑔 ) ( +_g ‘ 𝑄 ) ( 𝐻 ‘ ℎ ) ) )
61	1 9 10 11 12 14 18 19 54 55 56 57 58 60	isrhmd	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑃 RingHom 𝑄 ) )

Metamath Proof Explorer

Theorem selvply1rhm

Proof