mplmulmvr

Description: Multiply a polynomial F with a variable X (i.e. with a monic monomial). (Contributed by Thierry Arnoux, 25-Jan-2026)

	Ref	Expression
Hypotheses	mplmulmvr.1	$⊢ P = I mPoly R$
	mplmulmvr.2	$⊢ X = (I mVar R) (Y)$
	mplmulmvr.3	$⊢ M = {Base}_{P}$
	mplmulmvr.4	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	mplmulmvr.5	$⊢ \underset{˙}{0} = 0_{R}$
	mplmulmvr.6	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
	mplmulmvr.7	$⊢ A = 𝟙_{I} (\{Y\})$
	mplmulmvr.8	$⊢ φ \to I \in V$
	mplmulmvr.9	$⊢ φ \to Y \in I$
	mplmulmvr.10	$⊢ φ \to R \in Ring$
	mplmulmvr.11	$⊢ φ \to F \in M$
Assertion	mplmulmvr	$⊢ φ \to X \underset{˙}{\cdot} F = (b \in D ⟼ if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)))$

Proof

Step	Hyp	Ref	Expression
1		mplmulmvr.1	$⊢ P = I mPoly R$
2		mplmulmvr.2	$⊢ X = (I mVar R) (Y)$
3		mplmulmvr.3	$⊢ M = {Base}_{P}$
4		mplmulmvr.4	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		mplmulmvr.5	$⊢ \underset{˙}{0} = 0_{R}$
6		mplmulmvr.6	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
7		mplmulmvr.7	$⊢ A = 𝟙_{I} (\{Y\})$
8		mplmulmvr.8	$⊢ φ \to I \in V$
9		mplmulmvr.9	$⊢ φ \to Y \in I$
10		mplmulmvr.10	$⊢ φ \to R \in Ring$
11		mplmulmvr.11	$⊢ φ \to F \in M$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13	6	psrbasfsupp	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
14		eqid	$⊢ I mVar R = I mVar R$
15	1 14 3 8 10 9	mvrcl	$⊢ φ \to (I mVar R) (Y) \in M$
16	2 15	eqeltrid	$⊢ φ \to X \in M$
17	1 3 12 4 13 16 11	mplmul	$⊢ φ \to X \underset{˙}{\cdot} F = (b \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)))$
18		eqeq2	$⊢ \underset{˙}{0} = if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)) \to (\underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = \underset{˙}{0} \leftrightarrow \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)))$
19		eqeq2	$⊢ F (b -_{f} A) = if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)) \to (\underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = F (b -_{f} A) \leftrightarrow \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)))$
20		simplll	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to φ$
21		ssrab2	$⊢ \{y \in D \| y \leq_{f} b\} \subseteq D$
22	21	a1i	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to \{y \in D \| y \leq_{f} b\} \subseteq D$
23	22	sselda	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \in D$
24	2	fveq1i	$⊢ X (x) = (I mVar R) (Y) (x)$
25		eqid	$⊢ 1_{R} = 1_{R}$
26	8	adantr	$⊢ (φ \land x \in D) \to I \in V$
27	10	adantr	$⊢ (φ \land x \in D) \to R \in Ring$
28	9	adantr	$⊢ (φ \land x \in D) \to Y \in I$
29		simpr	$⊢ (φ \land x \in D) \to x \in D$
30	14 13 5 25 26 27 28 29 7	mvrvalind	$⊢ (φ \land x \in D) \to (I mVar R) (Y) (x) = if (x = A, 1_{R}, \underset{˙}{0})$
31	24 30	eqtrid	$⊢ (φ \land x \in D) \to X (x) = if (x = A, 1_{R}, \underset{˙}{0})$
32	20 23 31	syl2anc	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to X (x) = if (x = A, 1_{R}, \underset{˙}{0})$
33	32	oveq1d	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to X (x) \cdot_{R} F (b -_{f} x) = if (x = A, 1_{R}, \underset{˙}{0}) \cdot_{R} F (b -_{f} x)$
34		simpr	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x = A$
35	34	fveq1d	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x (Y) = A (Y)$
36		0ne1	$⊢ 0 \neq 1$
37	36	a1i	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to 0 \neq 1$
38	20 8	syl	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to I \in V$
39		nn0ex	$⊢ ℕ_{0} \in V$
40	39	a1i	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to ℕ_{0} \in V$
41	6	ssrab3	$⊢ D \subseteq {ℕ_{0}}^{I}$
42	22 41	sstrdi	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to \{y \in D \| y \leq_{f} b\} \subseteq {ℕ_{0}}^{I}$
43	42	sselda	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \in ({ℕ_{0}}^{I})$
44	38 40 43	elmaprd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x : I ⟶ ℕ_{0}$
45	44	adantr	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x : I ⟶ ℕ_{0}$
46	9	ad4antr	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to Y \in I$
47	45 46	ffvelcdmd	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x (Y) \in ℕ_{0}$
48	44	ffnd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x Fn I$
49	8	adantr	$⊢ (φ \land b \in D) \to I \in V$
50	39	a1i	$⊢ (φ \land b \in D) \to ℕ_{0} \in V$
51	41	a1i	$⊢ φ \to D \subseteq {ℕ_{0}}^{I}$
52	51	sselda	$⊢ (φ \land b \in D) \to b \in ({ℕ_{0}}^{I})$
53	49 50 52	elmaprd	$⊢ (φ \land b \in D) \to b : I ⟶ ℕ_{0}$
54	53	ad2antrr	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to b : I ⟶ ℕ_{0}$
55	54	ffnd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to b Fn I$
56		breq1	$⊢ y = x \to (y \leq_{f} b \leftrightarrow x \leq_{f} b)$
57		simpr	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \in \{y \in D \| y \leq_{f} b\}$
58	56 57	elrabrd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \leq_{f} b$
59	20 9	syl	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to Y \in I$
60	48 55 38 58 59	fnfvor	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x (Y) \leq b (Y)$
61	60	adantr	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x (Y) \leq b (Y)$
62		simpllr	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to b (Y) = 0$
63	61 62	breqtrd	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x (Y) \leq 0$
64		nn0le0eq0	$⊢ x (Y) \in ℕ_{0} \to (x (Y) \leq 0 \leftrightarrow x (Y) = 0)$
65	64	biimpa	$⊢ (x (Y) \in ℕ_{0} \land x (Y) \leq 0) \to x (Y) = 0$
66	47 63 65	syl2anc	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x (Y) = 0$
67	7	fveq1i	$⊢ A (Y) = 𝟙_{I} (\{Y\}) (Y)$
68	9	snssd	$⊢ φ \to \{Y\} \subseteq I$
69		snidg	$⊢ Y \in I \to Y \in \{Y\}$
70	9 69	syl	$⊢ φ \to Y \in \{Y\}$
71		ind1	$⊢ (I \in V \land \{Y\} \subseteq I \land Y \in \{Y\}) \to 𝟙_{I} (\{Y\}) (Y) = 1$
72	8 68 70 71	syl3anc	$⊢ φ \to 𝟙_{I} (\{Y\}) (Y) = 1$
73	67 72	eqtrid	$⊢ φ \to A (Y) = 1$
74	73	ad4antr	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to A (Y) = 1$
75	37 66 74	3netr4d	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to x (Y) \neq A (Y)$
76	75	neneqd	$⊢ ((((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to \neg x (Y) = A (Y)$
77	35 76	pm2.65da	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to \neg x = A$
78	77	iffalsed	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to if (x = A, 1_{R}, \underset{˙}{0}) = \underset{˙}{0}$
79	78	oveq1d	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to if (x = A, 1_{R}, \underset{˙}{0}) \cdot_{R} F (b -_{f} x) = \underset{˙}{0} \cdot_{R} F (b -_{f} x)$
80		eqid	$⊢ {Base}_{R} = {Base}_{R}$
81	20 10	syl	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to R \in Ring$
82	1 80 3 13 11	mplelf	$⊢ φ \to F : D ⟶ {Base}_{R}$
83	20 82	syl	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to F : D ⟶ {Base}_{R}$
84		simpllr	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to b \in D$
85	13	psrbagcon	$⊢ (b \in D \land x : I ⟶ ℕ_{0} \land x \leq_{f} b) \to (b -_{f} x \in D \land (b -_{f} x) \leq_{f} b)$
86	85	simpld	$⊢ (b \in D \land x : I ⟶ ℕ_{0} \land x \leq_{f} b) \to b -_{f} x \in D$
87	84 44 58 86	syl3anc	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to b -_{f} x \in D$
88	83 87	ffvelcdmd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to F (b -_{f} x) \in {Base}_{R}$
89	80 12 5 81 88	ringlzd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to \underset{˙}{0} \cdot_{R} F (b -_{f} x) = \underset{˙}{0}$
90	33 79 89	3eqtrd	$⊢ (((φ \land b \in D) \land b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to X (x) \cdot_{R} F (b -_{f} x) = \underset{˙}{0}$
91	90	mpteq2dva	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to (x \in \{y \in D \| y \leq_{f} b\} ⟼ X (x) \cdot_{R} F (b -_{f} x)) = (x \in \{y \in D \| y \leq_{f} b\} ⟼ \underset{˙}{0})$
92	91	oveq2d	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} \underset{˙}{0}$
93	10	ringgrpd	$⊢ φ \to R \in Grp$
94	93	grpmndd	$⊢ φ \to R \in Mnd$
95	94	ad2antrr	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to R \in Mnd$
96		ovex	$⊢ {ℕ_{0}}^{I} \in V$
97	6 96	rab2ex	$⊢ \{y \in D \| y \leq_{f} b\} \in V$
98	97	a1i	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to \{y \in D \| y \leq_{f} b\} \in V$
99	5	gsumz	$⊢ (R \in Mnd \land \{y \in D \| y \leq_{f} b\} \in V) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
100	95 98 99	syl2anc	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
101	92 100	eqtrd	$⊢ ((φ \land b \in D) \land b (Y) = 0) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = \underset{˙}{0}$
102		simplll	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to φ$
103	21	a1i	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to \{y \in D \| y \leq_{f} b\} \subseteq D$
104	103	sselda	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \in D$
105	102 104 31	syl2anc	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to X (x) = if (x = A, 1_{R}, \underset{˙}{0})$
106	105	oveq1d	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to X (x) \cdot_{R} F (b -_{f} x) = if (x = A, 1_{R}, \underset{˙}{0}) \cdot_{R} F (b -_{f} x)$
107		ovif	$⊢ if (x = A, 1_{R}, \underset{˙}{0}) \cdot_{R} F (b -_{f} x) = if (x = A, 1_{R} \cdot_{R} F (b -_{f} x), \underset{˙}{0} \cdot_{R} F (b -_{f} x))$
108	107	a1i	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to if (x = A, 1_{R}, \underset{˙}{0}) \cdot_{R} F (b -_{f} x) = if (x = A, 1_{R} \cdot_{R} F (b -_{f} x), \underset{˙}{0} \cdot_{R} F (b -_{f} x))$
109	102 10	syl	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to R \in Ring$
110	102 82	syl	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to F : D ⟶ {Base}_{R}$
111		simpllr	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to b \in D$
112	102 8	syl	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to I \in V$
113	39	a1i	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to ℕ_{0} \in V$
114	41 104	sselid	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \in ({ℕ_{0}}^{I})$
115	112 113 114	elmaprd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x : I ⟶ ℕ_{0}$
116		simpr	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \in \{y \in D \| y \leq_{f} b\}$
117	56 116	elrabrd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to x \leq_{f} b$
118	111 115 117 86	syl3anc	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to b -_{f} x \in D$
119	110 118	ffvelcdmd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to F (b -_{f} x) \in {Base}_{R}$
120	80 12 25 109 119	ringlidmd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to 1_{R} \cdot_{R} F (b -_{f} x) = F (b -_{f} x)$
121	120	adantr	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to 1_{R} \cdot_{R} F (b -_{f} x) = F (b -_{f} x)$
122		oveq2	$⊢ x = A \to b -_{f} x = b -_{f} A$
123	122	adantl	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to b -_{f} x = b -_{f} A$
124	123	fveq2d	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to F (b -_{f} x) = F (b -_{f} A)$
125	121 124	eqtrd	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land x = A) \to 1_{R} \cdot_{R} F (b -_{f} x) = F (b -_{f} A)$
126	80 12 5 109 119	ringlzd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to \underset{˙}{0} \cdot_{R} F (b -_{f} x) = \underset{˙}{0}$
127	126	adantr	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \land \neg x = A) \to \underset{˙}{0} \cdot_{R} F (b -_{f} x) = \underset{˙}{0}$
128	125 127	ifeq12da	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to if (x = A, 1_{R} \cdot_{R} F (b -_{f} x), \underset{˙}{0} \cdot_{R} F (b -_{f} x)) = if (x = A, F (b -_{f} A), \underset{˙}{0})$
129	106 108 128	3eqtrd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land x \in \{y \in D \| y \leq_{f} b\}) \to X (x) \cdot_{R} F (b -_{f} x) = if (x = A, F (b -_{f} A), \underset{˙}{0})$
130	129	mpteq2dva	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to (x \in \{y \in D \| y \leq_{f} b\} ⟼ X (x) \cdot_{R} F (b -_{f} x)) = (x \in \{y \in D \| y \leq_{f} b\} ⟼ if (x = A, F (b -_{f} A), \underset{˙}{0}))$
131	130	oveq2d	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} if (x = A, F (b -_{f} A), \underset{˙}{0})$
132	94	ad2antrr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to R \in Mnd$
133	97	a1i	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to \{y \in D \| y \leq_{f} b\} \in V$
134		breq1	$⊢ y = A \to (y \leq_{f} b \leftrightarrow A \leq_{f} b)$
135		breq1	$⊢ h = A \to ({finSupp}_{0} (h) \leftrightarrow {finSupp}_{0} (A))$
136	39	a1i	$⊢ φ \to ℕ_{0} \in V$
137		indf	$⊢ (I \in V \land \{Y\} \subseteq I) \to 𝟙_{I} (\{Y\}) : I ⟶ \{0, 1\}$
138	8 68 137	syl2anc	$⊢ φ \to 𝟙_{I} (\{Y\}) : I ⟶ \{0, 1\}$
139	7	feq1i	$⊢ A : I ⟶ \{0, 1\} \leftrightarrow 𝟙_{I} (\{Y\}) : I ⟶ \{0, 1\}$
140	138 139	sylibr	$⊢ φ \to A : I ⟶ \{0, 1\}$
141		0nn0	$⊢ 0 \in ℕ_{0}$
142	141	a1i	$⊢ φ \to 0 \in ℕ_{0}$
143		1nn0	$⊢ 1 \in ℕ_{0}$
144	143	a1i	$⊢ φ \to 1 \in ℕ_{0}$
145	142 144	prssd	$⊢ φ \to \{0, 1\} \subseteq ℕ_{0}$
146	140 145	fssd	$⊢ φ \to A : I ⟶ ℕ_{0}$
147	136 8 146	elmapdd	$⊢ φ \to A \in ({ℕ_{0}}^{I})$
148	146	ffund	$⊢ φ \to Fun A$
149	7	oveq1i	$⊢ A supp 0 = 𝟙_{I} (\{Y\}) supp 0$
150		indsupp	$⊢ (I \in V \land \{Y\} \subseteq I) \to 𝟙_{I} (\{Y\}) supp 0 = \{Y\}$
151	8 68 150	syl2anc	$⊢ φ \to 𝟙_{I} (\{Y\}) supp 0 = \{Y\}$
152	149 151	eqtrid	$⊢ φ \to A supp 0 = \{Y\}$
153		snfi	$⊢ \{Y\} \in Fin$
154	152 153	eqeltrdi	$⊢ φ \to A supp 0 \in Fin$
155	147 142 148 154	isfsuppd	$⊢ φ \to {finSupp}_{0} (A)$
156	135 147 155	elrabd	$⊢ φ \to A \in \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
157	156 6	eleqtrrdi	$⊢ φ \to A \in D$
158	157	ad2antrr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to A \in D$
159		breq1	$⊢ 1 = if (u \in \{Y\}, 1, 0) \to (1 \leq b (u) \leftrightarrow if (u \in \{Y\}, 1, 0) \leq b (u))$
160		breq1	$⊢ 0 = if (u \in \{Y\}, 1, 0) \to (0 \leq b (u) \leftrightarrow if (u \in \{Y\}, 1, 0) \leq b (u))$
161	53	adantr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to b : I ⟶ ℕ_{0}$
162	161	ffvelcdmda	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to b (u) \in ℕ_{0}$
163	162	adantr	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to b (u) \in ℕ_{0}$
164		elsni	$⊢ u \in \{Y\} \to u = Y$
165	164	adantl	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to u = Y$
166	165	fveq2d	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to b (u) = b (Y)$
167		simpllr	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to \neg b (Y) = 0$
168	167	neqned	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to b (Y) \neq 0$
169	166 168	eqnetrd	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to b (u) \neq 0$
170		elnnne0	$⊢ b (u) \in ℕ \leftrightarrow (b (u) \in ℕ_{0} \land b (u) \neq 0)$
171	163 169 170	sylanbrc	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to b (u) \in ℕ$
172	171	nnge1d	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land u \in \{Y\}) \to 1 \leq b (u)$
173	162	nn0ge0d	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to 0 \leq b (u)$
174	173	adantr	$⊢ ((((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \land \neg u \in \{Y\}) \to 0 \leq b (u)$
175	159 160 172 174	ifbothda	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to if (u \in \{Y\}, 1, 0) \leq b (u)$
176	175	ralrimiva	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to \forall u \in I if (u \in \{Y\}, 1, 0) \leq b (u)$
177	8	ad2antrr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to I \in V$
178	143	a1i	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to 1 \in ℕ_{0}$
179	141	a1i	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to 0 \in ℕ_{0}$
180	178 179	ifexd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to if (u \in \{Y\}, 1, 0) \in V$
181		fvexd	$⊢ (((φ \land b \in D) \land \neg b (Y) = 0) \land u \in I) \to b (u) \in V$
182		indval	$⊢ (I \in V \land \{Y\} \subseteq I) \to 𝟙_{I} (\{Y\}) = (u \in I ⟼ if (u \in \{Y\}, 1, 0))$
183	8 68 182	syl2anc	$⊢ φ \to 𝟙_{I} (\{Y\}) = (u \in I ⟼ if (u \in \{Y\}, 1, 0))$
184	7 183	eqtrid	$⊢ φ \to A = (u \in I ⟼ if (u \in \{Y\}, 1, 0))$
185	184	ad2antrr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to A = (u \in I ⟼ if (u \in \{Y\}, 1, 0))$
186	53	feqmptd	$⊢ (φ \land b \in D) \to b = (u \in I ⟼ b (u))$
187	186	adantr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to b = (u \in I ⟼ b (u))$
188	177 180 181 185 187	ofrfval2	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to (A \leq_{f} b \leftrightarrow \forall u \in I if (u \in \{Y\}, 1, 0) \leq b (u))$
189	176 188	mpbird	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to A \leq_{f} b$
190	134 158 189	elrabd	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to A \in \{y \in D \| y \leq_{f} b\}$
191		eqid	$⊢ (x \in \{y \in D \| y \leq_{f} b\} ⟼ if (x = A, F (b -_{f} A), \underset{˙}{0})) = (x \in \{y \in D \| y \leq_{f} b\} ⟼ if (x = A, F (b -_{f} A), \underset{˙}{0}))$
192	82	ad2antrr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to F : D ⟶ {Base}_{R}$
193		simplr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to b \in D$
194	146	ad2antrr	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to A : I ⟶ ℕ_{0}$
195	13	psrbagcon	$⊢ (b \in D \land A : I ⟶ ℕ_{0} \land A \leq_{f} b) \to (b -_{f} A \in D \land (b -_{f} A) \leq_{f} b)$
196	195	simpld	$⊢ (b \in D \land A : I ⟶ ℕ_{0} \land A \leq_{f} b) \to b -_{f} A \in D$
197	193 194 189 196	syl3anc	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to b -_{f} A \in D$
198	192 197	ffvelcdmd	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to F (b -_{f} A) \in {Base}_{R}$
199	5 132 133 190 191 198	gsummptif1n0	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} if (x = A, F (b -_{f} A), \underset{˙}{0}) = F (b -_{f} A)$
200	131 199	eqtrd	$⊢ ((φ \land b \in D) \land \neg b (Y) = 0) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = F (b -_{f} A)$
201	18 19 101 200	ifbothda	$⊢ (φ \land b \in D) \to \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x)) = if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A))$
202	201	mpteq2dva	$⊢ φ \to (b \in D ⟼ \underset{x \in \{y \in D \| y \leq_{f} b\}}{\sum_{R}} (X (x) \cdot_{R} F (b -_{f} x))) = (b \in D ⟼ if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)))$
203	17 202	eqtrd	$⊢ φ \to X \underset{˙}{\cdot} F = (b \in D ⟼ if (b (Y) = 0, \underset{˙}{0}, F (b -_{f} A)))$

Metamath Proof Explorer

Theorem mplmulmvr

Proof