mnringmulrcld

Description: Monoid rings are closed under multiplication. (Contributed by Rohan Ridenour, 14-May-2024)

	Ref	Expression
Hypotheses	mnringmulrcld.2	$⊢ F = R MndRing M$
	mnringmulrcld.3	$⊢ B = {Base}_{F}$
	mnringmulrcld.1	$⊢ A = {Base}_{M}$
	mnringmulrcld.4	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
	mnringmulrcld.5	$⊢ φ \to R \in Ring$
	mnringmulrcld.6	$⊢ φ \to M \in U$
	mnringmulrcld.7	$⊢ φ \to X \in B$
	mnringmulrcld.8	$⊢ φ \to Y \in B$
Assertion	mnringmulrcld	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$

Proof

Step	Hyp	Ref	Expression
1		mnringmulrcld.2	$⊢ F = R MndRing M$
2		mnringmulrcld.3	$⊢ B = {Base}_{F}$
3		mnringmulrcld.1	$⊢ A = {Base}_{M}$
4		mnringmulrcld.4	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
5		mnringmulrcld.5	$⊢ φ \to R \in Ring$
6		mnringmulrcld.6	$⊢ φ \to M \in U$
7		mnringmulrcld.7	$⊢ φ \to X \in B$
8		mnringmulrcld.8	$⊢ φ \to Y \in B$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		eqid	$⊢ 0_{R} = 0_{R}$
11		eqid	$⊢ +_{M} = +_{M}$
12	1 2 9 10 3 11 4 5 6 7 8	mnringmulrvald	$⊢ φ \to X \underset{˙}{\cdot} Y = \sum_{F} (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))$
13		eqid	$⊢ 0_{F} = 0_{F}$
14	1 5 6	mnringlmodd	$⊢ φ \to F \in LMod$
15		lmodcmn	$⊢ F \in LMod \to F \in CMnd$
16	14 15	syl	$⊢ φ \to F \in CMnd$
17	3	fvexi	$⊢ A \in V$
18	17 17	xpex	$⊢ A \times A \in V$
19	18	a1i	$⊢ φ \to A \times A \in V$
20	5	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to R \in Ring$
21		eqid	$⊢ {Base}_{R} = {Base}_{R}$
22	1 2 3 21 5 6 7	mnringbasefd	$⊢ φ \to X : A ⟶ {Base}_{R}$
23	22	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to X : A ⟶ {Base}_{R}$
24		simp2	$⊢ (φ \land a \in A \land b \in A) \to a \in A$
25	23 24	ffvelcdmd	$⊢ (φ \land a \in A \land b \in A) \to X (a) \in {Base}_{R}$
26	1 2 3 21 5 6 8	mnringbasefd	$⊢ φ \to Y : A ⟶ {Base}_{R}$
27	26	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to Y : A ⟶ {Base}_{R}$
28		simp3	$⊢ (φ \land a \in A \land b \in A) \to b \in A$
29	27 28	ffvelcdmd	$⊢ (φ \land a \in A \land b \in A) \to Y (b) \in {Base}_{R}$
30	21 9	ringcl	$⊢ (R \in Ring \land X (a) \in {Base}_{R} \land Y (b) \in {Base}_{R}) \to X (a) \cdot_{R} Y (b) \in {Base}_{R}$
31	20 25 29 30	syl3anc	$⊢ (φ \land a \in A \land b \in A) \to X (a) \cdot_{R} Y (b) \in {Base}_{R}$
32	21 10	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
33	20 32	syl	$⊢ (φ \land a \in A \land b \in A) \to 0_{R} \in {Base}_{R}$
34	31 33	ifcld	$⊢ (φ \land a \in A \land b \in A) \to if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}) \in {Base}_{R}$
35	34	adantr	$⊢ ((φ \land a \in A \land b \in A) \land i \in A) \to if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}) \in {Base}_{R}$
36	35	fmpttd	$⊢ (φ \land a \in A \land b \in A) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) : A ⟶ {Base}_{R}$
37	21	fvexi	$⊢ {Base}_{R} \in V$
38	37 17	elmap	$⊢ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in ({Base}_{R}^{A}) \leftrightarrow (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) : A ⟶ {Base}_{R}$
39	36 38	sylibr	$⊢ (φ \land a \in A \land b \in A) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in ({Base}_{R}^{A})$
40	17	a1i	$⊢ (φ \land a \in A \land b \in A) \to A \in V$
41		eqid	$⊢ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))$
42	40 33 41	sniffsupp	$⊢ (φ \land a \in A \land b \in A) \to {finSupp}_{0_{R}} ((i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))$
43	39 42	jca	$⊢ (φ \land a \in A \land b \in A) \to ((i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in ({Base}_{R}^{A}) \land {finSupp}_{0_{R}} ((i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))))$
44	6	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to M \in U$
45	1 2 3 21 10 20 44	mnringelbased	$⊢ (φ \land a \in A \land b \in A) \to ((i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in B \leftrightarrow ((i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in ({Base}_{R}^{A}) \land {finSupp}_{0_{R}} ((i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))))$
46	43 45	mpbird	$⊢ (φ \land a \in A \land b \in A) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in B$
47	46	3expb	$⊢ (φ \land (a \in A \land b \in A)) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in B$
48	47	ralrimivva	$⊢ φ \to \forall a \in A \forall b \in A (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in B$
49		eqid	$⊢ (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) = (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))$
50	49	fmpo	$⊢ \forall a \in A \forall b \in A (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in B \leftrightarrow (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) : A \times A ⟶ B$
51	48 50	sylib	$⊢ φ \to (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) : A \times A ⟶ B$
52	17 17	mpoex	$⊢ (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) \in V$
53	52	a1i	$⊢ φ \to (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) \in V$
54	51	ffnd	$⊢ φ \to (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) Fn (A \times A)$
55	13	fvexi	$⊢ 0_{F} \in V$
56	55	a1i	$⊢ φ \to 0_{F} \in V$
57	1 2 10 5 6 7	mnringbasefsuppd	$⊢ φ \to {finSupp}_{0_{R}} (X)$
58	57	fsuppimpd	$⊢ φ \to X supp 0_{R} \in Fin$
59	1 2 10 5 6 8	mnringbasefsuppd	$⊢ φ \to {finSupp}_{0_{R}} (Y)$
60	59	fsuppimpd	$⊢ φ \to Y supp 0_{R} \in Fin$
61		xpfi	$⊢ (X supp 0_{R} \in Fin \land Y supp 0_{R} \in Fin) \to {supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y) \in Fin$
62	58 60 61	syl2anc	$⊢ φ \to {supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y) \in Fin$
63		elxpi	$⊢ p \in (A \times A) \to \exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in A))$
64		simpl	$⊢ (p = ⟨a, b⟩ \land (a \in A \land b \in A)) \to p = ⟨a, b⟩$
65	64	2eximi	$⊢ \exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in A)) \to \exists a \exists b p = ⟨a, b⟩$
66	63 65	syl	$⊢ p \in (A \times A) \to \exists a \exists b p = ⟨a, b⟩$
67	66	adantl	$⊢ (φ \land p \in (A \times A)) \to \exists a \exists b p = ⟨a, b⟩$
68		nfv	$⊢ Ⅎ a (φ \land p \in (A \times A))$
69		nfv	$⊢ Ⅎ a p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y))$
70		nfmpo1	$⊢ \underline{Ⅎ} a (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))$
71		nfcv	$⊢ \underline{Ⅎ} a p$
72	70 71	nffv	$⊢ \underline{Ⅎ} a (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p)$
73		nfcv	$⊢ \underline{Ⅎ} a 0_{F}$
74	72 73	nfeq	$⊢ Ⅎ a (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F}$
75	69 74	nfor	$⊢ Ⅎ a (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F})$
76		nfv	$⊢ Ⅎ b (φ \land p \in (A \times A))$
77		nfv	$⊢ Ⅎ b p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y))$
78		nfmpo2	$⊢ \underline{Ⅎ} b (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))$
79		nfcv	$⊢ \underline{Ⅎ} b p$
80	78 79	nffv	$⊢ \underline{Ⅎ} b (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p)$
81		nfcv	$⊢ \underline{Ⅎ} b 0_{F}$
82	80 81	nfeq	$⊢ Ⅎ b (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F}$
83	77 82	nfor	$⊢ Ⅎ b (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F})$
84		simp3	$⊢ (φ \land p \in (A \times A) \land p = ⟨a, b⟩) \to p = ⟨a, b⟩$
85		simp2	$⊢ (φ \land p \in (A \times A) \land p = ⟨a, b⟩) \to p \in (A \times A)$
86	84 85	eqeltrrd	$⊢ (φ \land p \in (A \times A) \land p = ⟨a, b⟩) \to ⟨a, b⟩ \in (A \times A)$
87		opelxp	$⊢ ⟨a, b⟩ \in (A \times A) \leftrightarrow (a \in A \land b \in A)$
88	86 87	sylib	$⊢ (φ \land p \in (A \times A) \land p = ⟨a, b⟩) \to (a \in A \land b \in A)$
89		ianor	$⊢ \neg (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)) \leftrightarrow (\neg a \in {supp}_{0_{R}} (X) \lor \neg b \in {supp}_{0_{R}} (Y))$
90	22	ffnd	$⊢ φ \to X Fn A$
91	17	a1i	$⊢ φ \to A \in V$
92	10	fvexi	$⊢ 0_{R} \in V$
93	92	a1i	$⊢ φ \to 0_{R} \in V$
94		elsuppfn	$⊢ (X Fn A \land A \in V \land 0_{R} \in V) \to (a \in {supp}_{0_{R}} (X) \leftrightarrow (a \in A \land X (a) \neq 0_{R}))$
95	90 91 93 94	syl3anc	$⊢ φ \to (a \in {supp}_{0_{R}} (X) \leftrightarrow (a \in A \land X (a) \neq 0_{R}))$
96	95	biimprd	$⊢ φ \to ((a \in A \land X (a) \neq 0_{R}) \to a \in {supp}_{0_{R}} (X))$
97	96	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to ((a \in A \land X (a) \neq 0_{R}) \to a \in {supp}_{0_{R}} (X))$
98	24 97	mpand	$⊢ (φ \land a \in A \land b \in A) \to (X (a) \neq 0_{R} \to a \in {supp}_{0_{R}} (X))$
99	98	necon1bd	$⊢ (φ \land a \in A \land b \in A) \to (\neg a \in {supp}_{0_{R}} (X) \to X (a) = 0_{R})$
100	26	ffnd	$⊢ φ \to Y Fn A$
101		elsuppfn	$⊢ (Y Fn A \land A \in V \land 0_{R} \in V) \to (b \in {supp}_{0_{R}} (Y) \leftrightarrow (b \in A \land Y (b) \neq 0_{R}))$
102	100 91 93 101	syl3anc	$⊢ φ \to (b \in {supp}_{0_{R}} (Y) \leftrightarrow (b \in A \land Y (b) \neq 0_{R}))$
103	102	biimprd	$⊢ φ \to ((b \in A \land Y (b) \neq 0_{R}) \to b \in {supp}_{0_{R}} (Y))$
104	103	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to ((b \in A \land Y (b) \neq 0_{R}) \to b \in {supp}_{0_{R}} (Y))$
105	28 104	mpand	$⊢ (φ \land a \in A \land b \in A) \to (Y (b) \neq 0_{R} \to b \in {supp}_{0_{R}} (Y))$
106	105	necon1bd	$⊢ (φ \land a \in A \land b \in A) \to (\neg b \in {supp}_{0_{R}} (Y) \to Y (b) = 0_{R})$
107	99 106	orim12d	$⊢ (φ \land a \in A \land b \in A) \to ((\neg a \in {supp}_{0_{R}} (X) \lor \neg b \in {supp}_{0_{R}} (Y)) \to (X (a) = 0_{R} \lor Y (b) = 0_{R}))$
108	107	imp	$⊢ ((φ \land a \in A \land b \in A) \land (\neg a \in {supp}_{0_{R}} (X) \lor \neg b \in {supp}_{0_{R}} (Y))) \to (X (a) = 0_{R} \lor Y (b) = 0_{R})$
109	89 108	sylan2b	$⊢ ((φ \land a \in A \land b \in A) \land \neg (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y))) \to (X (a) = 0_{R} \lor Y (b) = 0_{R})$
110		oveq1	$⊢ X (a) = 0_{R} \to X (a) \cdot_{R} Y (b) = 0_{R} \cdot_{R} Y (b)$
111	21 9 10	ringlz	$⊢ (R \in Ring \land Y (b) \in {Base}_{R}) \to 0_{R} \cdot_{R} Y (b) = 0_{R}$
112	20 29 111	syl2anc	$⊢ (φ \land a \in A \land b \in A) \to 0_{R} \cdot_{R} Y (b) = 0_{R}$
113	110 112	sylan9eqr	$⊢ ((φ \land a \in A \land b \in A) \land X (a) = 0_{R}) \to X (a) \cdot_{R} Y (b) = 0_{R}$
114		oveq2	$⊢ Y (b) = 0_{R} \to X (a) \cdot_{R} Y (b) = X (a) \cdot_{R} 0_{R}$
115	21 9 10	ringrz	$⊢ (R \in Ring \land X (a) \in {Base}_{R}) \to X (a) \cdot_{R} 0_{R} = 0_{R}$
116	20 25 115	syl2anc	$⊢ (φ \land a \in A \land b \in A) \to X (a) \cdot_{R} 0_{R} = 0_{R}$
117	114 116	sylan9eqr	$⊢ ((φ \land a \in A \land b \in A) \land Y (b) = 0_{R}) \to X (a) \cdot_{R} Y (b) = 0_{R}$
118	113 117	jaodan	$⊢ ((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \to X (a) \cdot_{R} Y (b) = 0_{R}$
119	118	adantr	$⊢ (((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \land i = a +_{M} b) \to X (a) \cdot_{R} Y (b) = 0_{R}$
120		eqidd	$⊢ (((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \land \neg i = a +_{M} b) \to 0_{R} = 0_{R}$
121	119 120	ifeqda	$⊢ ((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \to if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}) = 0_{R}$
122	121	mpteq2dv	$⊢ ((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = (i \in A ⟼ 0_{R})$
123		fconstmpt	$⊢ A \times \{0_{R}\} = (i \in A ⟼ 0_{R})$
124	1 10 3 5 6	mnring0g2d	$⊢ φ \to A \times \{0_{R}\} = 0_{F}$
125	123 124	eqtr3id	$⊢ φ \to (i \in A ⟼ 0_{R}) = 0_{F}$
126	125	3ad2ant1	$⊢ (φ \land a \in A \land b \in A) \to (i \in A ⟼ 0_{R}) = 0_{F}$
127	126	adantr	$⊢ ((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \to (i \in A ⟼ 0_{R}) = 0_{F}$
128	122 127	eqtrd	$⊢ ((φ \land a \in A \land b \in A) \land (X (a) = 0_{R} \lor Y (b) = 0_{R})) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F}$
129	109 128	syldan	$⊢ ((φ \land a \in A \land b \in A) \land \neg (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y))) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F}$
130	129	ex	$⊢ (φ \land a \in A \land b \in A) \to (\neg (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F})$
131	130	orrd	$⊢ (φ \land a \in A \land b \in A) \to ((a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)) \lor (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F})$
132	131	3expb	$⊢ (φ \land (a \in A \land b \in A)) \to ((a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)) \lor (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F})$
133	132	3adant3	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to ((a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)) \lor (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F})$
134		eleq1	$⊢ p = ⟨a, b⟩ \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \leftrightarrow ⟨a, b⟩ \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)))$
135		opelxp	$⊢ ⟨a, b⟩ \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \leftrightarrow (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y))$
136	134 135	bitrdi	$⊢ p = ⟨a, b⟩ \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \leftrightarrow (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)))$
137	136	3ad2ant3	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \leftrightarrow (a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)))$
138		simp2l	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to a \in A$
139		simp2r	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to b \in A$
140		eqidd	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) = (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})))$
141		simp3	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to p = ⟨a, b⟩$
142	17	mptex	$⊢ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in V$
143	142	a1i	$⊢ ((φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \land a \in A \land b \in A) \to (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) \in V$
144	140 141 143	fvmpopr2d	$⊢ ((φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \land a \in A \land b \in A) \to (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))$
145	138 139 144	mpd3an23	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))$
146	145	eqeq1d	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to ((a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F} \leftrightarrow (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F})$
147	137 146	orbi12d	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to ((p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F}) \leftrightarrow ((a \in {supp}_{0_{R}} (X) \land b \in {supp}_{0_{R}} (Y)) \lor (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R})) = 0_{F}))$
148	133 147	mpbird	$⊢ (φ \land (a \in A \land b \in A) \land p = ⟨a, b⟩) \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F})$
149	88 148	syld3an2	$⊢ (φ \land p \in (A \times A) \land p = ⟨a, b⟩) \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F})$
150	149	3expia	$⊢ (φ \land p \in (A \times A)) \to (p = ⟨a, b⟩ \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F}))$
151	76 83 150	exlimd	$⊢ (φ \land p \in (A \times A)) \to (\exists b p = ⟨a, b⟩ \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F}))$
152	68 75 151	exlimd	$⊢ (φ \land p \in (A \times A)) \to (\exists a \exists b p = ⟨a, b⟩ \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F}))$
153	67 152	mpd	$⊢ (φ \land p \in (A \times A)) \to (p \in ({supp}_{0_{R}} (X) \times {supp}_{0_{R}} (Y)) \lor (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) (p) = 0_{F})$
154	53 54 56 62 153	finnzfsuppd	$⊢ φ \to {finSupp}_{0_{F}} ((a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))))$
155	2 13 16 19 51 154	gsumcl	$⊢ φ \to \sum_{F} (a \in A, b \in A ⟼ (i \in A ⟼ if (i = a +_{M} b, X (a) \cdot_{R} Y (b), 0_{R}))) \in B$
156	12 155	eqeltrd	$⊢ φ \to X \underset{˙}{\cdot} Y \in B$

Metamath Proof Explorer

Theorem mnringmulrcld

Proof