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