rhmply1mon

Description: Apply a ring homomorphism between two univariate polynomial algebras to a scaled monomial, as in ply1coe . (Contributed by SN, 20-May-2025)

	Ref	Expression
Hypotheses	rhmply1mon.p	$⊢ P = {Poly}_{1} (R)$
	rhmply1mon.q	$⊢ Q = {Poly}_{1} (S)$
	rhmply1mon.b	$⊢ B = {Base}_{P}$
	rhmply1mon.k	$⊢ K = {Base}_{R}$
	rhmply1mon.f	$⊢ F = (p \in B ⟼ H \circ p)$
	rhmply1mon.x	$⊢ X = {var}_{1} (R)$
	rhmply1mon.y	$⊢ Y = {var}_{1} (S)$
	rhmply1mon.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	rhmply1mon.u	$⊢ \underset{˙}{∙} = \cdot_{Q}$
	rhmply1mon.m	$⊢ M = {mulGrp}_{P}$
	rhmply1mon.n	$⊢ N = {mulGrp}_{Q}$
	rhmply1mon.l	$⊢ \underset{˙}{\times} = \cdot_{M}$
	rhmply1mon.w	$⊢ \underset{˙}{\land} = \cdot_{N}$
	rhmply1mon.h	$⊢ φ \to H \in (R RingHom S)$
	rhmply1mon.c	$⊢ φ \to C \in K$
	rhmply1mon.e	$⊢ φ \to E \in ℕ_{0}$
Assertion	rhmply1mon	$⊢ φ \to F (C \underset{˙}{\cdot} (E \underset{˙}{\times} X)) = H (C) \underset{˙}{∙} (E \underset{˙}{\land} Y)$

Proof

Step	Hyp	Ref	Expression
1		rhmply1mon.p	$⊢ P = {Poly}_{1} (R)$
2		rhmply1mon.q	$⊢ Q = {Poly}_{1} (S)$
3		rhmply1mon.b	$⊢ B = {Base}_{P}$
4		rhmply1mon.k	$⊢ K = {Base}_{R}$
5		rhmply1mon.f	$⊢ F = (p \in B ⟼ H \circ p)$
6		rhmply1mon.x	$⊢ X = {var}_{1} (R)$
7		rhmply1mon.y	$⊢ Y = {var}_{1} (S)$
8		rhmply1mon.t	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
9		rhmply1mon.u	$⊢ \underset{˙}{∙} = \cdot_{Q}$
10		rhmply1mon.m	$⊢ M = {mulGrp}_{P}$
11		rhmply1mon.n	$⊢ N = {mulGrp}_{Q}$
12		rhmply1mon.l	$⊢ \underset{˙}{\times} = \cdot_{M}$
13		rhmply1mon.w	$⊢ \underset{˙}{\land} = \cdot_{N}$
14		rhmply1mon.h	$⊢ φ \to H \in (R RingHom S)$
15		rhmply1mon.c	$⊢ φ \to C \in K$
16		rhmply1mon.e	$⊢ φ \to E \in ℕ_{0}$
17	10 3	mgpbas	$⊢ B = {Base}_{M}$
18		rhmrcl1	$⊢ H \in (R RingHom S) \to R \in Ring$
19	14 18	syl	$⊢ φ \to R \in Ring$
20	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
21	19 20	syl	$⊢ φ \to P \in Ring$
22	10	ringmgp	$⊢ P \in Ring \to M \in Mnd$
23	21 22	syl	$⊢ φ \to M \in Mnd$
24	6 1 3	vr1cl	$⊢ R \in Ring \to X \in B$
25	19 24	syl	$⊢ φ \to X \in B$
26	17 12 23 16 25	mulgnn0cld	$⊢ φ \to E \underset{˙}{\times} X \in B$
27	1 2 3 4 5 8 9 14 15 26	rhmply1vsca	$⊢ φ \to F (C \underset{˙}{\cdot} (E \underset{˙}{\times} X)) = H (C) \underset{˙}{∙} F (E \underset{˙}{\times} X)$
28	1 2 3 5 14	rhmply1	$⊢ φ \to F \in (P RingHom Q)$
29	10 11	rhmmhm	$⊢ F \in (P RingHom Q) \to F \in (M MndHom N)$
30	28 29	syl	$⊢ φ \to F \in (M MndHom N)$
31	17 12 13	mhmmulg	$⊢ (F \in (M MndHom N) \land E \in ℕ_{0} \land X \in B) \to F (E \underset{˙}{\times} X) = E \underset{˙}{\land} F (X)$
32	30 16 25 31	syl3anc	$⊢ φ \to F (E \underset{˙}{\times} X) = E \underset{˙}{\land} F (X)$
33	1 2 3 5 6 7 14	rhmply1vr1	$⊢ φ \to F (X) = Y$
34	33	oveq2d	$⊢ φ \to E \underset{˙}{\land} F (X) = E \underset{˙}{\land} Y$
35	32 34	eqtrd	$⊢ φ \to F (E \underset{˙}{\times} X) = E \underset{˙}{\land} Y$
36	35	oveq2d	$⊢ φ \to H (C) \underset{˙}{∙} F (E \underset{˙}{\times} X) = H (C) \underset{˙}{∙} (E \underset{˙}{\land} Y)$
37	27 36	eqtrd	$⊢ φ \to F (C \underset{˙}{\cdot} (E \underset{˙}{\times} X)) = H (C) \underset{˙}{∙} (E \underset{˙}{\land} Y)$

Metamath Proof Explorer

Theorem rhmply1mon

Proof