Metamath Proof Explorer

Theorem 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 ⊢ B = Base P
selvply1rhm.2 ⊢ P = I mPoly R
selvply1rhm.3 ⊢ U = I ∖ X mPoly R
selvply1rhm.4 ⊢ Q = Poly 1 ⁡ U
selvply1rhm.5 ⊢ H = f ∈ B ⟼ n ∈ ℕ 0 1 𝑜 ⟼ I selectVars R ⁡ X ⁡ f ⁡ X n ⁡ ∅
selvply1rhm.6 ⊢ φ → I ∈ V
selvply1rhm.7 ⊢ φ → X ∈ I
selvply1rhm.8 ⊢ φ → R ∈ CRing
Assertion selvply1rhm ⊢ φ → H ∈ P RingHom Q

Proof

Step Hyp Ref Expression
1 selvply1rhm.1 ⊢ B = Base P
2 selvply1rhm.2 ⊢ P = I mPoly R
3 selvply1rhm.3 ⊢ U = I ∖ X mPoly R
4 selvply1rhm.4 ⊢ Q = Poly 1 ⁡ U
5 selvply1rhm.5 ⊢ H = f ∈ B ⟼ n ∈ ℕ 0 1 𝑜 ⟼ I selectVars R ⁡ X ⁡ f ⁡ X n ⁡ ∅
6 selvply1rhm.6 ⊢ φ → I ∈ V
7 selvply1rhm.7 ⊢ φ → X ∈ I
8 selvply1rhm.8 ⊢ φ → R ∈ CRing
9 eqid ⊢ 1 P = 1 P
10 eqid ⊢ 1 Q = 1 Q
11 eqid ⊢ ⋅ P = ⋅ P
12 eqid ⊢ ⋅ Q = ⋅ Q
13 8 crngringd ⊢ φ → R ∈ Ring
14 2 6 13 mplringd ⊢ φ → P ∈ Ring
15 6 difexd ⊢ φ → I ∖ X ∈ V
16 3 15 13 mplringd ⊢ φ → U ∈ Ring
17 4 ply1ring ⊢ U ∈ Ring → Q ∈ Ring
18 16 17 syl ⊢ φ → Q ∈ Ring
19 1 2 3 4 5 6 7 8 selvply1rhmlem2 ⊢ φ → H ⁡ 1 P = 1 Q
20 eqid ⊢ Base X mPoly U = Base X mPoly U
21 eqid ⊢ X mPoly U = X mPoly U
22 eqid ⊢ ⋅ X mPoly U = ⋅ X mPoly U
23 fveq1 ⊢ p = q → p ⁡ X r ⁡ ∅ = q ⁡ X r ⁡ ∅
24 23 mpteq2dv ⊢ p = q → r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ = r ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X r ⁡ ∅
25 24 cbvmptv ⊢ p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ = q ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X r ⁡ ∅
26 fveq1 ⊢ r = s → r ⁡ ∅ = s ⁡ ∅
27 26 opeq2d ⊢ r = s → X r ⁡ ∅ = X s ⁡ ∅
28 27 sneqd ⊢ r = s → X r ⁡ ∅ = X s ⁡ ∅
29 28 fveq2d ⊢ r = s → q ⁡ X r ⁡ ∅ = q ⁡ X s ⁡ ∅
30 29 cbvmptv ⊢ r ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X r ⁡ ∅ = s ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X s ⁡ ∅
31 30 mpteq2i ⊢ q ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X r ⁡ ∅ = q ∈ Base X mPoly U ⟼ s ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X s ⁡ ∅
32 25 31 eqtri ⊢ p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ = q ∈ Base X mPoly U ⟼ s ∈ ℕ 0 1 𝑜 ⟼ q ⁡ X s ⁡ ∅
33 7 ad2antrr ⊢ φ ∧ g ∈ B ∧ h ∈ B → X ∈ I
34 16 ad2antrr ⊢ φ ∧ g ∈ B ∧ h ∈ B → U ∈ Ring
35 8 ad2antrr ⊢ φ ∧ g ∈ B ∧ h ∈ B → R ∈ CRing
36 7 snssd ⊢ φ → X ⊆ I
37 36 ad2antrr ⊢ φ ∧ g ∈ B ∧ h ∈ B → X ⊆ I
38 simplr ⊢ φ ∧ g ∈ B ∧ h ∈ B → g ∈ B
39 2 1 3 21 20 35 37 38 selvcl ⊢ φ ∧ g ∈ B ∧ h ∈ B → I selectVars R ⁡ X ⁡ g ∈ Base X mPoly U
40 simpr ⊢ φ ∧ g ∈ B ∧ h ∈ B → h ∈ B
41 2 1 3 21 20 35 37 40 selvcl ⊢ φ ∧ g ∈ B ∧ h ∈ B → I selectVars R ⁡ X ⁡ h ∈ Base X mPoly U
42 20 21 22 12 4 32 33 34 39 41 selvply1rhmlemb ⊢ φ ∧ g ∈ B ∧ h ∈ B → p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ X mPoly U I selectVars R ⁡ X ⁡ h = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ Q p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ h
43 6 ad2antrr ⊢ φ ∧ g ∈ B ∧ h ∈ B → I ∈ V
44 14 ad2antrr ⊢ φ ∧ g ∈ B ∧ h ∈ B → P ∈ Ring
45 1 11 44 38 40 ringcld ⊢ φ ∧ g ∈ B ∧ h ∈ B → g ⋅ P h ∈ B
46 1 2 3 4 5 43 33 35 45 25 selvply1rhmlem5 ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g ⋅ P h = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ P h
47 2 1 11 3 21 22 43 35 37 38 40 selvmul ⊢ φ ∧ g ∈ B ∧ h ∈ B → I selectVars R ⁡ X ⁡ g ⋅ P h = I selectVars R ⁡ X ⁡ g ⋅ X mPoly U I selectVars R ⁡ X ⁡ h
48 47 fveq2d ⊢ φ ∧ g ∈ B ∧ h ∈ B → p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ P h = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ X mPoly U I selectVars R ⁡ X ⁡ h
49 46 48 eqtrd ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g ⋅ P h = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ X mPoly U I selectVars R ⁡ X ⁡ h
50 1 2 3 4 5 43 33 35 38 25 selvply1rhmlem5 ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g
51 1 2 3 4 5 43 33 35 40 25 selvply1rhmlem5 ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ h = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ h
52 50 51 oveq12d ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g ⋅ Q H ⁡ h = p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ g ⋅ Q p ∈ Base X mPoly U ⟼ r ∈ ℕ 0 1 𝑜 ⟼ p ⁡ X r ⁡ ∅ ⁡ I selectVars R ⁡ X ⁡ h
53 42 49 52 3eqtr4d ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g ⋅ P h = H ⁡ g ⋅ Q H ⁡ h
54 53 anasss ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g ⋅ P h = H ⁡ g ⋅ Q H ⁡ h
55 eqid ⊢ Base Q = Base Q
56 eqid ⊢ + P = + P
57 eqid ⊢ + Q = + Q
58 1 2 3 4 5 6 7 8 selvply1rhmlem1 ⊢ φ → H : B ⟶ Base Q
59 1 2 3 4 5 43 33 35 38 40 selvply1rhmlem4 ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g + P h = H ⁡ g + Q H ⁡ h
60 59 anasss ⊢ φ ∧ g ∈ B ∧ h ∈ B → H ⁡ g + P h = H ⁡ g + Q H ⁡ h
61 1 9 10 11 12 14 18 19 54 55 56 57 58 60 isrhmd ⊢ φ → H ∈ P RingHom Q