Theorem rprmdvdsprod

Description: If a prime element Q divides a product, then it divides one term. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmdvdsprod.b	$$⊢B={\mathrm{Base}}_R$$
	rprmdvdsprod.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
	rprmdvdsprod.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
	rprmdvdsprod.1	$$⊢\underset{\dot{}}{1}=1_R$$
	rprmdvdsprod.m	$$⊢M={\mathrm{mulGrp}}_R$$
	rprmdvdsprod.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	rprmdvdsprod.q	$$⊢\phi \to Q\in P$$
	rprmdvdsprod.i	$$⊢\phi \to I\in V$$
	rprmdvdsprod.2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{1}}\left(F\right)$$
	rprmdvdsprod.f	$$⊢\phi \to F:I⟶B$$
	rprmdvdsprod.3	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left({\sum }_M,F\right)$$
Assertion	rprmdvdsprod	$$⊢\phi \to \exists x\in {supp}_{\underset{\dot{}}{1}}\left(F\right)Q\underset{\dot{}}{\parallel }F\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		rprmdvdsprod.b	$$⊢B={\mathrm{Base}}_R$$
2		rprmdvdsprod.p	$$⊢P=\mathrm{RPrime}\left(R\right)$$
3		rprmdvdsprod.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(R\right)$$
4		rprmdvdsprod.1	$$⊢\underset{\dot{}}{1}=1_R$$
5		rprmdvdsprod.m	$$⊢M={\mathrm{mulGrp}}_R$$
6		rprmdvdsprod.r	$$⊢\phi \to R\in \mathrm{CRing}$$
7		rprmdvdsprod.q	$$⊢\phi \to Q\in P$$
8		rprmdvdsprod.i	$$⊢\phi \to I\in V$$
9		rprmdvdsprod.2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{1}}\left(F\right)$$
10		rprmdvdsprod.f	$$⊢\phi \to F:I⟶B$$
11		rprmdvdsprod.3	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left({\sum }_M,F\right)$$
12	5 1	mgpbas	$$⊢B={\mathrm{Base}}_M$$
13	5 4	ringidval	$$⊢\underset{\dot{}}{1}=0_M$$
14		eqid	$$⊢{\cdot }_R={\cdot }_R$$
15	5 14	mgpplusg	$$⊢{\cdot }_R={+}_M$$
16	5	crngmgp	$$⊢R\in \mathrm{CRing}\to M\in \mathrm{CMnd}$$
17	6 16	syl	$$⊢\phi \to M\in \mathrm{CMnd}$$
18		disjdifr	$$⊢\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\cap {supp}_{\underset{\dot{}}{1}}\left(F\right)=\varnothing$$
19	18	a1i	$$⊢\phi \to \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\cap {supp}_{\underset{\dot{}}{1}}\left(F\right)=\varnothing$$
20		suppssdm	$$⊢F\mathrm{supp}\underset{\dot{}}{1}\subseteq \mathrm{dom}F$$
21	20 10	fssdm	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{1}\subseteq I$$
22		undifr	$$⊢F\mathrm{supp}\underset{\dot{}}{1}\subseteq I\leftrightarrow \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\cup {supp}_{\underset{\dot{}}{1}}\left(F\right)=I$$
23	21 22	sylib	$$⊢\phi \to \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\cup {supp}_{\underset{\dot{}}{1}}\left(F\right)=I$$
24	23	eqcomd	$$⊢\phi \to I=\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\cup {supp}_{\underset{\dot{}}{1}}\left(F\right)$$
25	12 13 15 17 8 10 9 19 24	gsumsplit	$$⊢\phi \to {\sum }_{M}F=\left({\sum }_M,\left({F\upharpoonright }_{\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)}\right)\right){\cdot }_R\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)$$
26		difssd	$$⊢\phi \to I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\subseteq I$$
27	10 26	feqresmpt	$$⊢\phi \to {F\upharpoonright }_{\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)}=\left(z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)⟼F\left(z\right)\right)$$
28	10	ffnd	$$⊢\phi \to FFnI$$
29	28	adantr	$$⊢\left(\phi \wedge z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\right)\to FFnI$$
30	8	adantr	$$⊢\left(\phi \wedge z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\right)\to I\in V$$
31	6	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
32	1 4	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
33	31 32	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
34	33	adantr	$$⊢\left(\phi \wedge z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\right)\to \underset{\dot{}}{1}\in B$$
35		simpr	$$⊢\left(\phi \wedge z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\right)\to z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)$$
36	29 30 34 35	fvdifsupp	$$⊢\left(\phi \wedge z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)\right)\to F\left(z\right)=\underset{\dot{}}{1}$$
37	36	mpteq2dva	$$⊢\phi \to \left(z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)⟼F\left(z\right)\right)=\left(z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)⟼\underset{\dot{}}{1}\right)$$
38	27 37	eqtrd	$$⊢\phi \to {F\upharpoonright }_{\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)}=\left(z\in \left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)⟼\underset{\dot{}}{1}\right)$$
39	38	oveq2d	$$⊢\phi \to {\sum }_M\left({F\upharpoonright }_{\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)}\right)=\underset{z\in I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)}{{\sum }_M}\underset{\dot{}}{1}$$
40	17	cmnmndd	$$⊢\phi \to M\in \mathrm{Mnd}$$
41	8	difexd	$$⊢\phi \to I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\in \mathrm{V}$$
42	13	gsumz	$$⊢\left(M\in \mathrm{Mnd}\wedge I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\in \mathrm{V}\right)\to \underset{z\in I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)}{{\sum }_M}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
43	40 41 42	syl2anc	$$⊢\phi \to \underset{z\in I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)}{{\sum }_M}\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
44	39 43	eqtrd	$$⊢\phi \to {\sum }_M\left({F\upharpoonright }_{\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)}\right)=\underset{\dot{}}{1}$$
45	44	oveq1d	$$⊢\phi \to \left({\sum }_M,\left({F\upharpoonright }_{\left(I\setminus {supp}_{\underset{\dot{}}{1}}\left(F\right)\right)}\right)\right){\cdot }_R\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)=\underset{\dot{}}{1}{\cdot }_R\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)$$
46		ovexd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{1}\in \mathrm{V}$$
47	10 21	fssresd	$$⊢\phi \to \left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right):F\mathrm{supp}\underset{\dot{}}{1}⟶B$$
48	9 33	fsuppres	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{1}}\left(\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)$$
49	12 13 17 46 47 48	gsumcl	$$⊢\phi \to {\sum }_M\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\in B$$
50	1 14 4 31 49	ringlidmd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_R\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)={\sum }_M\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)$$
51	25 45 50	3eqtrd	$$⊢\phi \to {\sum }_{M}F={\sum }_M\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)$$
52	11 51	breqtrd	$$⊢\phi \to Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)$$
53		reseq2	$$⊢b=\varnothing \to {F\upharpoonright }_b={F\upharpoonright }_{\varnothing }$$
54	53	oveq2d	$$⊢b=\varnothing \to {\sum }_M\left({F\upharpoonright }_b\right)={\sum }_M\left({F\upharpoonright }_{\varnothing }\right)$$
55	54	breq2d	$$⊢b=\varnothing \to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\right)$$
56		rexeq	$$⊢b=\varnothing \to \left(\exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow \exists x\in \varnothing Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
57	55 56	imbi12d	$$⊢b=\varnothing \to \left(\left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\to \exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\to \exists x\in \varnothing Q\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)$$
58		reseq2	$$⊢b=a\to {F\upharpoonright }_b={F\upharpoonright }_a$$
59	58	oveq2d	$$⊢b=a\to {\sum }_M\left({F\upharpoonright }_b\right)={\sum }_M\left({F\upharpoonright }_a\right)$$
60	59	breq2d	$$⊢b=a\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\right)$$
61		rexeq	$$⊢b=a\to \left(\exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
62	60 61	imbi12d	$$⊢b=a\to \left(\left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\to \exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)$$
63		reseq2	$$⊢b=a\cup \left\{y\right\}\to {F\upharpoonright }_b={F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}$$
64	63	oveq2d	$$⊢b=a\cup \left\{y\right\}\to {\sum }_M\left({F\upharpoonright }_b\right)={\sum }_M\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)$$
65	64	breq2d	$$⊢b=a\cup \left\{y\right\}\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)$$
66		rexeq	$$⊢b=a\cup \left\{y\right\}\to \left(\exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow \exists x\in \left(a\cup \left\{y\right\}\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
67	65 66	imbi12d	$$⊢b=a\cup \left\{y\right\}\to \left(\left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\to \exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\to \exists x\in \left(a\cup \left\{y\right\}\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)$$
68		reseq2	$$⊢b=F\mathrm{supp}\underset{\dot{}}{1}\to {F\upharpoonright }_b={F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}$$
69	68	oveq2d	$$⊢b=F\mathrm{supp}\underset{\dot{}}{1}\to {\sum }_M\left({F\upharpoonright }_b\right)={\sum }_M\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)$$
70	69	breq2d	$$⊢b=F\mathrm{supp}\underset{\dot{}}{1}\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)\right)$$
71		rexeq	$$⊢b=F\mathrm{supp}\underset{\dot{}}{1}\to \left(\exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow \exists x\in {supp}_{\underset{\dot{}}{1}}\left(F\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
72	70 71	imbi12d	$$⊢b=F\mathrm{supp}\underset{\dot{}}{1}\to \left(\left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_b\right)\right)\to \exists x\in bQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\leftrightarrow \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)\to \exists x\in {supp}_{\underset{\dot{}}{1}}\left(F\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)$$
73	4 3 2 6 7	rprmndvdsr1	$$⊢\phi \to \neg Q\underset{\dot{}}{\parallel }\underset{\dot{}}{1}$$
74		res0	$$⊢{F\upharpoonright }_{\varnothing }=\varnothing$$
75	74	oveq2i	$$⊢{\sum }_M\left({F\upharpoonright }_{\varnothing }\right)={\sum }_M\varnothing$$
76	13	gsum0	$$⊢{\sum }_M\varnothing =\underset{\dot{}}{1}$$
77	75 76	eqtri	$$⊢{\sum }_M\left({F\upharpoonright }_{\varnothing }\right)=\underset{\dot{}}{1}$$
78	77	a1i	$$⊢\phi \to {\sum }_M\left({F\upharpoonright }_{\varnothing }\right)=\underset{\dot{}}{1}$$
79	78	breq2d	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\leftrightarrow Q\underset{\dot{}}{\parallel }\underset{\dot{}}{1}\right)$$
80	73 79	mtbird	$$⊢\phi \to \neg Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)$$
81	80	pm2.21d	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\varnothing }\right)\right)\to \exists x\in \varnothing Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
82		simpllr	$$⊢\left(\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
83	82	syldbl2	$$⊢\left(\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)$$
84		vex	$$⊢y\in \mathrm{V}$$
85		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
86	85	breq2d	$$⊢x=y\to \left(Q\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow Q\underset{\dot{}}{\parallel }F\left(y\right)\right)$$
87	84 86	rexsn	$$⊢\exists x\in \left\{y\right\}Q\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow Q\underset{\dot{}}{\parallel }F\left(y\right)$$
88	87	bilanri	$$⊢\left(\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }F\left(y\right)\right)\to \exists x\in \left\{y\right\}Q\underset{\dot{}}{\parallel }F\left(x\right)$$
89	6	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to R\in \mathrm{CRing}$$
90	7	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to Q\in P$$
91	89 16	syl	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to M\in \mathrm{CMnd}$$
92		vex	$$⊢a\in \mathrm{V}$$
93	92	a1i	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to a\in \mathrm{V}$$
94	10	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to F:I⟶B$$
95		simp-4r	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to a\subseteq F\mathrm{supp}\underset{\dot{}}{1}$$
96	21	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to F\mathrm{supp}\underset{\dot{}}{1}\subseteq I$$
97	95 96	sstrd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to a\subseteq I$$
98	94 97	fssresd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \left({F\upharpoonright }_a\right):a⟶B$$
99	9	fsuppimpd	$$⊢\phi \to F\mathrm{supp}\underset{\dot{}}{1}\in \mathrm{Fin}$$
100	99	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to F\mathrm{supp}\underset{\dot{}}{1}\in \mathrm{Fin}$$
101	100 95	ssfid	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to a\in \mathrm{Fin}$$
102	33	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \underset{\dot{}}{1}\in B$$
103	98 101 102	fdmfifsupp	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to {finSupp}_{\underset{\dot{}}{1}}\left(\left({F\upharpoonright }_a\right)\right)$$
104	12 13 91 93 98 103	gsumcl	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to {\sum }_M\left({F\upharpoonright }_a\right)\in B$$
105	96	ssdifssd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to {supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\subseteq I$$
106		simpllr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)$$
107	105 106	sseldd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to y\in I$$
108	94 107	ffvelcdmd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to F\left(y\right)\in B$$
109		simpr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)$$
110		eqid	$$⊢\mathrm{Cntz}\left(M\right)=\mathrm{Cntz}\left(M\right)$$
111		eqid	$$⊢F\left(y\right)=F\left(y\right)$$
112	40	ad4antr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to M\in \mathrm{Mnd}$$
113	106	eldifbd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \neg y\in a$$
114	94	fimassd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to F\left[a\cup \left\{y\right\}\right]\subseteq B$$
115	12 110	cntzcmn	$$⊢\left(M\in \mathrm{CMnd}\wedge F\left[a\cup \left\{y\right\}\right]\subseteq B\right)\to \mathrm{Cntz}\left(M\right)\left(F\left[a\cup \left\{y\right\}\right]\right)=B$$
116	91 114 115	syl2anc	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \mathrm{Cntz}\left(M\right)\left(F\left[a\cup \left\{y\right\}\right]\right)=B$$
117	114 116	sseqtrrd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to F\left[a\cup \left\{y\right\}\right]\subseteq \mathrm{Cntz}\left(M\right)\left(F\left[a\cup \left\{y\right\}\right]\right)$$
118	12 15 110 111 94 97 112 101 113 107 108 117	gsumzresunsn	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to {\sum }_M\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)=\left({\sum }_M,\left({F\upharpoonright }_a\right)\right){\cdot }_{R}F\left(y\right)$$
119	109 118	breqtrd	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to Q\underset{\dot{}}{\parallel }\left(\left({\sum }_M,\left({F\upharpoonright }_a\right)\right){\cdot }_{R}F\left(y\right)\right)$$
120	1 2 3 14 89 90 104 108 119	rprmdvds	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\vee Q\underset{\dot{}}{\parallel }F\left(y\right)\right)$$
121	83 88 120	orim12da	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \left(\exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\vee \exists x\in \left\{y\right\}Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
122		rexun	$$⊢\exists x\in \left(a\cup \left\{y\right\}\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\leftrightarrow \left(\exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\vee \exists x\in \left\{y\right\}Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
123	121 122	sylibr	$$⊢\left(\left(\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\wedge \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)\wedge Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\right)\to \exists x\in \left(a\cup \left\{y\right\}\right)Q\underset{\dot{}}{\parallel }F\left(x\right)$$
124	123	exp31	$$⊢\left(\left(\phi \wedge a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\right)\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\to \left(\left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\to \exists x\in \left(a\cup \left\{y\right\}\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)$$
125	124	anasss	$$⊢\left(\phi \wedge \left(a\subseteq F\mathrm{supp}\underset{\dot{}}{1}\wedge y\in \left({supp}_{\underset{\dot{}}{1}}\left(F\right)\setminus a\right)\right)\right)\to \left(\left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_a\right)\right)\to \exists x\in aQ\underset{\dot{}}{\parallel }F\left(x\right)\right)\to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{\left(a\cup \left\{y\right\}\right)}\right)\right)\to \exists x\in \left(a\cup \left\{y\right\}\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)\right)$$
126	57 62 67 72 81 125 99	findcard2d	$$⊢\phi \to \left(Q\underset{\dot{}}{\parallel }\left({\sum }_M,\left({F\upharpoonright }_{{supp}_{\underset{\dot{}}{1}}\left(F\right)}\right)\right)\to \exists x\in {supp}_{\underset{\dot{}}{1}}\left(F\right)Q\underset{\dot{}}{\parallel }F\left(x\right)\right)$$
127	52 126	mpd	$$⊢\phi \to \exists x\in {supp}_{\underset{\dot{}}{1}}\left(F\right)Q\underset{\dot{}}{\parallel }F\left(x\right)$$