selvmul

Description: The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025)

	Ref	Expression
Hypotheses	selvmul.p	$⊢ P = I mPoly R$
	selvmul.b	$⊢ B = {Base}_{P}$
	selvmul.1	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	selvmul.u	$⊢ U = (I ∖ J) mPoly R$
	selvmul.t	$⊢ T = J mPoly U$
	selvmul.2	$⊢ \underset{˙}{∙} = \cdot_{T}$
	selvmul.i	$⊢ φ \to I \in V$
	selvmul.r	$⊢ φ \to R \in CRing$
	selvmul.j	$⊢ φ \to J \subseteq I$
	selvmul.f	$⊢ φ \to F \in B$
	selvmul.g	$⊢ φ \to G \in B$
Assertion	selvmul	$⊢ φ \to (I selectVars R) (J) (F \underset{˙}{\cdot} G) = (I selectVars R) (J) (F) \underset{˙}{∙} (I selectVars R) (J) (G)$

Proof

Step	Hyp	Ref	Expression
1		selvmul.p	$⊢ P = I mPoly R$
2		selvmul.b	$⊢ B = {Base}_{P}$
3		selvmul.1	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
4		selvmul.u	$⊢ U = (I ∖ J) mPoly R$
5		selvmul.t	$⊢ T = J mPoly U$
6		selvmul.2	$⊢ \underset{˙}{∙} = \cdot_{T}$
7		selvmul.i	$⊢ φ \to I \in V$
8		selvmul.r	$⊢ φ \to R \in CRing$
9		selvmul.j	$⊢ φ \to J \subseteq I$
10		selvmul.f	$⊢ φ \to F \in B$
11		selvmul.g	$⊢ φ \to G \in B$
12		eqid	$⊢ I mPoly T = I mPoly T$
13		eqid	$⊢ {Base}_{(I mPoly T)} = {Base}_{(I mPoly T)}$
14		eqid	$⊢ \cdot_{(I mPoly T)} = \cdot_{(I mPoly T)}$
15		eqid	$⊢ algSc (T) = algSc (T)$
16		eqid	$⊢ algSc (T) \circ algSc (U) = algSc (T) \circ algSc (U)$
17	7	difexd	$⊢ φ \to I ∖ J \in V$
18	7 9	ssexd	$⊢ φ \to J \in V$
19	4 5 15 16 17 18 8	selvcllem2	$⊢ φ \to algSc (T) \circ algSc (U) \in (R RingHom T)$
20	1 12 2 13 3 14 7 19 10 11	rhmcomulmpl	$⊢ φ \to (algSc (T) \circ algSc (U)) \circ (F \underset{˙}{\cdot} G) = ((algSc (T) \circ algSc (U)) \circ F) \cdot_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G)$
21	20	fveq2d	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{\cdot} G)) = (I eval T) (((algSc (T) \circ algSc (U)) \circ F) \cdot_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G))$
22	21	fveq1d	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{\cdot} G)) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) (((algSc (T) \circ algSc (U)) \circ F) \cdot_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G)) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
23		eqid	$⊢ I eval T = I eval T$
24		eqid	$⊢ {Base}_{T} = {Base}_{T}$
25	4 17 8	mplcrngd	$⊢ φ \to U \in CRing$
26	5 18 25	mplcrngd	$⊢ φ \to T \in CRing$
27		eqid	$⊢ (x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))) = (x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))$
28	4 5 15 24 27 7 8 9	selvcllem5	$⊢ φ \to (x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))) \in ({Base}_{T}^{I})$
29		rhmghm	$⊢ algSc (T) \circ algSc (U) \in (R RingHom T) \to algSc (T) \circ algSc (U) \in (R GrpHom T)$
30		ghmmhm	$⊢ algSc (T) \circ algSc (U) \in (R GrpHom T) \to algSc (T) \circ algSc (U) \in (R MndHom T)$
31	19 29 30	3syl	$⊢ φ \to algSc (T) \circ algSc (U) \in (R MndHom T)$
32	1 12 2 13 7 31 10	mhmcompl	$⊢ φ \to (algSc (T) \circ algSc (U)) \circ F \in {Base}_{(I mPoly T)}$
33		eqidd	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
34	32 33	jca	$⊢ φ \to ((algSc (T) \circ algSc (U)) \circ F \in {Base}_{(I mPoly T)} \land (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))))$
35	1 12 2 13 7 31 11	mhmcompl	$⊢ φ \to (algSc (T) \circ algSc (U)) \circ G \in {Base}_{(I mPoly T)}$
36		eqidd	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
37	35 36	jca	$⊢ φ \to ((algSc (T) \circ algSc (U)) \circ G \in {Base}_{(I mPoly T)} \land (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))))$
38	23 12 24 13 14 6 7 26 28 34 37	evlmulval	$⊢ φ \to (((algSc (T) \circ algSc (U)) \circ F) \cdot_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G) \in {Base}_{(I mPoly T)} \land (I eval T) (((algSc (T) \circ algSc (U)) \circ F) \cdot_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G)) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) \underset{˙}{∙} (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))))$
39	38	simprd	$⊢ φ \to (I eval T) (((algSc (T) \circ algSc (U)) \circ F) \cdot_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G)) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) \underset{˙}{∙} (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
40	22 39	eqtrd	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{\cdot} G)) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) \underset{˙}{∙} (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
41	1 7 8	mplcrngd	$⊢ φ \to P \in CRing$
42	41	crngringd	$⊢ φ \to P \in Ring$
43	2 3 42 10 11	ringcld	$⊢ φ \to F \underset{˙}{\cdot} G \in B$
44	1 2 4 5 15 16 7 8 9 43	selvval2	$⊢ φ \to (I selectVars R) (J) (F \underset{˙}{\cdot} G) = (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{\cdot} G)) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
45	1 2 4 5 15 16 7 8 9 10	selvval2	$⊢ φ \to (I selectVars R) (J) (F) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
46	1 2 4 5 15 16 7 8 9 11	selvval2	$⊢ φ \to (I selectVars R) (J) (G) = (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
47	45 46	oveq12d	$⊢ φ \to (I selectVars R) (J) (F) \underset{˙}{∙} (I selectVars R) (J) (G) = (I eval T) ((algSc (T) \circ algSc (U)) \circ F) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x))))) \underset{˙}{∙} (I eval T) ((algSc (T) \circ algSc (U)) \circ G) ((x \in I ⟼ if (x \in J, (J mVar U) (x), algSc (T) (((I ∖ J) mVar R) (x)))))$
48	40 44 47	3eqtr4d	$⊢ φ \to (I selectVars R) (J) (F \underset{˙}{\cdot} G) = (I selectVars R) (J) (F) \underset{˙}{∙} (I selectVars R) (J) (G)$

Metamath Proof Explorer

Theorem selvmul

Proof