rhmcomulmpl

Description: Show that the ring homomorphism in rhmmpl preserves multiplication. (Contributed by SN, 8-Feb-2025)

	Ref	Expression
Hypotheses	rhmcomulmpl.p	$⊢ P = I mPoly R$
	rhmcomulmpl.q	$⊢ Q = I mPoly S$
	rhmcomulmpl.b	$⊢ B = {Base}_{P}$
	rhmcomulmpl.c	$⊢ C = {Base}_{Q}$
	rhmcomulmpl.1	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	rhmcomulmpl.2	$⊢ \underset{˙}{∙} = \cdot_{Q}$
	rhmcomulmpl.i	$⊢ φ \to I \in V$
	rhmcomulmpl.h	$⊢ φ \to H \in (R RingHom S)$
	rhmcomulmpl.f	$⊢ φ \to F \in B$
	rhmcomulmpl.g	$⊢ φ \to G \in B$
Assertion	rhmcomulmpl	$⊢ φ \to H \circ (F \underset{˙}{\cdot} G) = (H \circ F) \underset{˙}{∙} (H \circ G)$

Proof

Step	Hyp	Ref	Expression
1		rhmcomulmpl.p	$⊢ P = I mPoly R$
2		rhmcomulmpl.q	$⊢ Q = I mPoly S$
3		rhmcomulmpl.b	$⊢ B = {Base}_{P}$
4		rhmcomulmpl.c	$⊢ C = {Base}_{Q}$
5		rhmcomulmpl.1	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
6		rhmcomulmpl.2	$⊢ \underset{˙}{∙} = \cdot_{Q}$
7		rhmcomulmpl.i	$⊢ φ \to I \in V$
8		rhmcomulmpl.h	$⊢ φ \to H \in (R RingHom S)$
9		rhmcomulmpl.f	$⊢ φ \to F \in B$
10		rhmcomulmpl.g	$⊢ φ \to G \in B$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13	11 12	rhmf	$⊢ H \in (R RingHom S) \to H : {Base}_{R} ⟶ {Base}_{S}$
14	8 13	syl	$⊢ φ \to H : {Base}_{R} ⟶ {Base}_{S}$
15		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
16		rhmrcl1	$⊢ H \in (R RingHom S) \to R \in Ring$
17	8 16	syl	$⊢ φ \to R \in Ring$
18	1 11 3 15 9	mplelf	$⊢ φ \to F : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
19	1 11 3 15 10	mplelf	$⊢ φ \to G : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
20	15 17 18 19	rhmmpllem2	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d)) \in {Base}_{R}$
21	14 20	cofmpt	$⊢ φ \to H \circ (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d))) = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ H (\underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d))))$
22		eqid	$⊢ 0_{R} = 0_{R}$
23	17	ringcmnd	$⊢ φ \to R \in CMnd$
24	23	adantr	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to R \in CMnd$
25		rhmrcl2	$⊢ H \in (R RingHom S) \to S \in Ring$
26	8 25	syl	$⊢ φ \to S \in Ring$
27	26	ringgrpd	$⊢ φ \to S \in Grp$
28	27	grpmndd	$⊢ φ \to S \in Mnd$
29	28	adantr	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to S \in Mnd$
30		ovex	$⊢ {ℕ_{0}}^{I} \in V$
31	30	rabex	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \in V$
32	31	rabex	$⊢ \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} \in V$
33	32	a1i	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} \in V$
34		rhmghm	$⊢ H \in (R RingHom S) \to H \in (R GrpHom S)$
35		ghmmhm	$⊢ H \in (R GrpHom S) \to H \in (R MndHom S)$
36	8 34 35	3syl	$⊢ φ \to H \in (R MndHom S)$
37	36	adantr	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to H \in (R MndHom S)$
38		eqid	$⊢ \cdot_{R} = \cdot_{R}$
39	17	ad2antrr	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to R \in Ring$
40	18	ad2antrr	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to F : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
41		breq1	$⊢ e = d \to (e \leq_{f} k \leftrightarrow d \leq_{f} k)$
42	41	elrab	$⊢ d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} \leftrightarrow (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land d \leq_{f} k)$
43	42	biimpi	$⊢ d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} \to (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land d \leq_{f} k)$
44	43	adantl	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land d \leq_{f} k)$
45	44	simpld	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
46	40 45	ffvelcdmd	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to F (d) \in {Base}_{R}$
47	19	ad2antrr	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to G : \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟶ {Base}_{R}$
48		simplr	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
49	15	psrbagf	$⊢ d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \to d : I ⟶ ℕ_{0}$
50	45 49	syl	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to d : I ⟶ ℕ_{0}$
51	44	simprd	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to d \leq_{f} k$
52	15	psrbagcon	$⊢ (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land d : I ⟶ ℕ_{0} \land d \leq_{f} k) \to (k -_{f} d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land (k -_{f} d) \leq_{f} k)$
53	48 50 51 52	syl3anc	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to (k -_{f} d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \land (k -_{f} d) \leq_{f} k)$
54	53	simpld	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to k -_{f} d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
55	47 54	ffvelcdmd	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to G (k -_{f} d) \in {Base}_{R}$
56	11 38 39 46 55	ringcld	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to F (d) \cdot_{R} G (k -_{f} d) \in {Base}_{R}$
57	15 17 18 19	rhmmpllem1	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to {finSupp}_{0_{R}} ((d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} ⟼ F (d) \cdot_{R} G (k -_{f} d)))$
58	11 22 24 29 33 37 56 57	gsummptmhm	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} H (F (d) \cdot_{R} G (k -_{f} d)) = H (\underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d)))$
59	8	ad2antrr	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to H \in (R RingHom S)$
60		eqid	$⊢ \cdot_{S} = \cdot_{S}$
61	11 38 60	rhmmul	$⊢ (H \in (R RingHom S) \land F (d) \in {Base}_{R} \land G (k -_{f} d) \in {Base}_{R}) \to H (F (d) \cdot_{R} G (k -_{f} d)) = H (F (d)) \cdot_{S} H (G (k -_{f} d))$
62	59 46 55 61	syl3anc	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to H (F (d) \cdot_{R} G (k -_{f} d)) = H (F (d)) \cdot_{S} H (G (k -_{f} d))$
63	40 45	fvco3d	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to (H \circ F) (d) = H (F (d))$
64	47 54	fvco3d	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to (H \circ G) (k -_{f} d) = H (G (k -_{f} d))$
65	63 64	oveq12d	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to (H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d) = H (F (d)) \cdot_{S} H (G (k -_{f} d))$
66	62 65	eqtr4d	$⊢ ((φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \land d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}) \to H (F (d) \cdot_{R} G (k -_{f} d)) = (H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d)$
67	66	mpteq2dva	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to (d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} ⟼ H (F (d) \cdot_{R} G (k -_{f} d))) = (d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\} ⟼ (H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d))$
68	67	oveq2d	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} H (F (d) \cdot_{R} G (k -_{f} d)) = \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} ((H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d))$
69	58 68	eqtr3d	$⊢ (φ \land k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to H (\underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d))) = \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} ((H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d))$
70	69	mpteq2dva	$⊢ φ \to (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ H (\underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d)))) = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} ((H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d)))$
71	21 70	eqtrd	$⊢ φ \to H \circ (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d))) = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} ((H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d)))$
72	1 3 38 5 15 9 10	mplmul	$⊢ φ \to F \underset{˙}{\cdot} G = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d)))$
73	72	coeq2d	$⊢ φ \to H \circ (F \underset{˙}{\cdot} G) = H \circ (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{R}} (F (d) \cdot_{R} G (k -_{f} d)))$
74	1 2 3 4 7 36 9	mhmcompl	$⊢ φ \to H \circ F \in C$
75	1 2 3 4 7 36 10	mhmcompl	$⊢ φ \to H \circ G \in C$
76	2 4 60 6 15 74 75	mplmul	$⊢ φ \to (H \circ F) \underset{˙}{∙} (H \circ G) = (k \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ \underset{d \in \{e \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} \| e \leq_{f} k\}}{\sum_{S}} ((H \circ F) (d) \cdot_{S} (H \circ G) (k -_{f} d)))$
77	71 73 76	3eqtr4d	$⊢ φ \to H \circ (F \underset{˙}{\cdot} G) = (H \circ F) \underset{˙}{∙} (H \circ G)$

Metamath Proof Explorer

Theorem rhmcomulmpl

Proof