selvadd

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

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

Proof

Step	Hyp	Ref	Expression
1		selvadd.p	$⊢ P = I mPoly R$
2		selvadd.b	$⊢ B = {Base}_{P}$
3		selvadd.1	$⊢ \underset{˙}{+} = +_{P}$
4		selvadd.u	$⊢ U = (I ∖ J) mPoly R$
5		selvadd.t	$⊢ T = J mPoly U$
6		selvadd.2	$⊢ \underset{˙}{✚} = +_{T}$
7		selvadd.i	$⊢ φ \to I \in V$
8		selvadd.r	$⊢ φ \to R \in CRing$
9		selvadd.j	$⊢ φ \to J \subseteq I$
10		selvadd.f	$⊢ φ \to F \in B$
11		selvadd.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	$⊢ +_{(I mPoly T)} = +_{(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		rhmghm	$⊢ algSc (T) \circ algSc (U) \in (R RingHom T) \to algSc (T) \circ algSc (U) \in (R GrpHom T)$
21		ghmmhm	$⊢ algSc (T) \circ algSc (U) \in (R GrpHom T) \to algSc (T) \circ algSc (U) \in (R MndHom T)$
22	19 20 21	3syl	$⊢ φ \to algSc (T) \circ algSc (U) \in (R MndHom T)$
23	1 12 2 13 3 14 7 22 10 11	mhmcoaddmpl	$⊢ φ \to (algSc (T) \circ algSc (U)) \circ (F \underset{˙}{+} G) = ((algSc (T) \circ algSc (U)) \circ F) +_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G)$
24	23	fveq2d	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{+} G)) = (I eval T) (((algSc (T) \circ algSc (U)) \circ F) +_{(I mPoly T)} ((algSc (T) \circ algSc (U)) \circ G))$
25	24	fveq1d	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{+} 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) +_{(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)))))$
26		eqid	$⊢ I eval T = I eval T$
27		eqid	$⊢ {Base}_{T} = {Base}_{T}$
28	4 17 8	mplcrngd	$⊢ φ \to U \in CRing$
29	5 18 28	mplcrngd	$⊢ φ \to T \in CRing$
30		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))))$
31	4 5 15 27 30 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})$
32	1 12 2 13 7 22 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 22 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	26 12 27 13 14 6 7 29 31 34 37	evladdval	$⊢ φ \to (((algSc (T) \circ algSc (U)) \circ F) +_{(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) +_{(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) +_{(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	25 39	eqtrd	$⊢ φ \to (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{+} 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	crnggrpd	$⊢ φ \to P \in Grp$
43	2 3 42 10 11	grpcld	$⊢ φ \to F \underset{˙}{+} G \in B$
44	1 2 4 5 15 16 7 8 9 43	selvval2	$⊢ φ \to (I selectVars R) (J) (F \underset{˙}{+} G) = (I eval T) ((algSc (T) \circ algSc (U)) \circ (F \underset{˙}{+} 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{˙}{+} G) = (I selectVars R) (J) (F) \underset{˙}{✚} (I selectVars R) (J) (G)$

Metamath Proof Explorer

Theorem selvadd

Proof