Theorem ablfac1eulem

Description: Lemma for ablfac1eu . (Contributed by Mario Carneiro, 27-Apr-2016)

	Ref	Expression
Hypotheses	ablfac1.b	$$⊢B={\mathrm{Base}}_G$$
	ablfac1.o	$$⊢O=\mathrm{od}\left(G\right)$$
	ablfac1.s	$$⊢S=\left(p\in A⟼\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\right)$$
	ablfac1.g	$$⊢\phi \to G\in \mathrm{Abel}$$
	ablfac1.f	$$⊢\phi \to B\in \mathrm{Fin}$$
	ablfac1.1	$$⊢\phi \to A\subseteq \mathbb{P}$$
	ablfac1c.d	$$⊢D=\left\{w\in \mathbb{P}|w\parallel \left|B\right|\right\}$$
	ablfac1.2	$$⊢\phi \to D\subseteq A$$
	ablfac1eu.1	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}T\wedge G\mathrm{DProd}T=B\right)$$
	ablfac1eu.2	$$⊢\phi \to \mathrm{dom}T=A$$
	ablfac1eu.3	$$⊢\left(\phi \wedge q\in A\right)\to C\in {\mathbb{N}}_0$$
	ablfac1eu.4	$$⊢\left(\phi \wedge q\in A\right)\to \left|T\left(q\right)\right|=q^C$$
	ablfac1eulem.1	$$⊢\phi \to P\in \mathbb{P}$$
	ablfac1eulem.2	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	ablfac1eulem	$$⊢\phi \to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|$$

Proof

Step	Hyp	Ref	Expression
1		ablfac1.b	$$⊢B={\mathrm{Base}}_G$$
2		ablfac1.o	$$⊢O=\mathrm{od}\left(G\right)$$
3		ablfac1.s	$$⊢S=\left(p\in A⟼\left\{x\in B|O\left(x\right)\parallel p^{p\mathrm{pCnt}\left|B\right|}\right\}\right)$$
4		ablfac1.g	$$⊢\phi \to G\in \mathrm{Abel}$$
5		ablfac1.f	$$⊢\phi \to B\in \mathrm{Fin}$$
6		ablfac1.1	$$⊢\phi \to A\subseteq \mathbb{P}$$
7		ablfac1c.d	$$⊢D=\left\{w\in \mathbb{P}|w\parallel \left|B\right|\right\}$$
8		ablfac1.2	$$⊢\phi \to D\subseteq A$$
9		ablfac1eu.1	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}T\wedge G\mathrm{DProd}T=B\right)$$
10		ablfac1eu.2	$$⊢\phi \to \mathrm{dom}T=A$$
11		ablfac1eu.3	$$⊢\left(\phi \wedge q\in A\right)\to C\in {\mathbb{N}}_0$$
12		ablfac1eu.4	$$⊢\left(\phi \wedge q\in A\right)\to \left|T\left(q\right)\right|=q^C$$
13		ablfac1eulem.1	$$⊢\phi \to P\in \mathbb{P}$$
14		ablfac1eulem.2	$$⊢\phi \to A\in \mathrm{Fin}$$
15		ssid	$$⊢A\subseteq A$$
16		sseq1	$$⊢y=\varnothing \to \left(y\subseteq A\leftrightarrow \varnothing \subseteq A\right)$$
17		difeq1	$$⊢y=\varnothing \to y\setminus \left\{P\right\}=\varnothing \setminus \left\{P\right\}$$
18		0dif	$$⊢\varnothing \setminus \left\{P\right\}=\varnothing$$
19	17 18	eqtrdi	$$⊢y=\varnothing \to y\setminus \left\{P\right\}=\varnothing$$
20	19	reseq2d	$$⊢y=\varnothing \to {T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\varnothing }$$
21		res0	$$⊢{T\upharpoonright }_{\varnothing }=\varnothing$$
22	20 21	eqtrdi	$$⊢y=\varnothing \to {T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}=\varnothing$$
23	22	oveq2d	$$⊢y=\varnothing \to G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\varnothing$$
24	23	fveq2d	$$⊢y=\varnothing \to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\varnothing \right|$$
25	24	breq2d	$$⊢y=\varnothing \to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel \left|G\mathrm{DProd}\varnothing \right|\right)$$
26	25	notbid	$$⊢y=\varnothing \to \left(\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \neg P\parallel \left|G\mathrm{DProd}\varnothing \right|\right)$$
27	16 26	imbi12d	$$⊢y=\varnothing \to \left(\left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\leftrightarrow \left(\varnothing \subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\varnothing \right|\right)\right)$$
28	27	imbi2d	$$⊢y=\varnothing \to \left(\left(\phi \to \left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\varnothing \right|\right)\right)\right)$$
29		sseq1	$$⊢y=z\to \left(y\subseteq A\leftrightarrow z\subseteq A\right)$$
30		difeq1	$$⊢y=z\to y\setminus \left\{P\right\}=z\setminus \left\{P\right\}$$
31	30	reseq2d	$$⊢y=z\to {T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}$$
32	31	oveq2d	$$⊢y=z\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)$$
33	32	fveq2d	$$⊢y=z\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|$$
34	33	breq2d	$$⊢y=z\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)$$
35	34	notbid	$$⊢y=z\to \left(\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)$$
36	29 35	imbi12d	$$⊢y=z\to \left(\left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\leftrightarrow \left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
37	36	imbi2d	$$⊢y=z\to \left(\left(\phi \to \left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\leftrightarrow \left(\phi \to \left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\right)$$
38		sseq1	$$⊢y=z\cup \left\{q\right\}\to \left(y\subseteq A\leftrightarrow z\cup \left\{q\right\}\subseteq A\right)$$
39		difeq1	$$⊢y=z\cup \left\{q\right\}\to y\setminus \left\{P\right\}=\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}$$
40	39	reseq2d	$$⊢y=z\cup \left\{q\right\}\to {T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}$$
41	40	oveq2d	$$⊢y=z\cup \left\{q\right\}\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)$$
42	41	fveq2d	$$⊢y=z\cup \left\{q\right\}\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|$$
43	42	breq2d	$$⊢y=z\cup \left\{q\right\}\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)$$
44	43	notbid	$$⊢y=z\cup \left\{q\right\}\to \left(\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)$$
45	38 44	imbi12d	$$⊢y=z\cup \left\{q\right\}\to \left(\left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\leftrightarrow \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
46	45	imbi2d	$$⊢y=z\cup \left\{q\right\}\to \left(\left(\phi \to \left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\leftrightarrow \left(\phi \to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\right)$$
47		sseq1	$$⊢y=A\to \left(y\subseteq A\leftrightarrow A\subseteq A\right)$$
48		difeq1	$$⊢y=A\to y\setminus \left\{P\right\}=A\setminus \left\{P\right\}$$
49	48	reseq2d	$$⊢y=A\to {T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}$$
50	49	oveq2d	$$⊢y=A\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)$$
51	50	fveq2d	$$⊢y=A\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|$$
52	51	breq2d	$$⊢y=A\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|\right)$$
53	52	notbid	$$⊢y=A\to \left(\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|\right)$$
54	47 53	imbi12d	$$⊢y=A\to \left(\left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\leftrightarrow \left(A\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
55	54	imbi2d	$$⊢y=A\to \left(\left(\phi \to \left(y\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(y\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\leftrightarrow \left(\phi \to \left(A\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\right)$$
56		nprmdvds1	$$⊢P\in \mathbb{P}\to \neg P\parallel 1$$
57	13 56	syl	$$⊢\phi \to \neg P\parallel 1$$
58		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
59		eqid	$$⊢0_G=0_G$$
60	59	dprd0	$$⊢G\in \mathrm{Grp}\to \left(G\mathrm{dom}\mathrm{DProd}\varnothing \wedge G\mathrm{DProd}\varnothing =\left\{0_G\right\}\right)$$
61	4 58 60	3syl	$$⊢\phi \to \left(G\mathrm{dom}\mathrm{DProd}\varnothing \wedge G\mathrm{DProd}\varnothing =\left\{0_G\right\}\right)$$
62	61	simprd	$$⊢\phi \to G\mathrm{DProd}\varnothing =\left\{0_G\right\}$$
63	62	fveq2d	$$⊢\phi \to \left|G\mathrm{DProd}\varnothing \right|=\left|\left\{0_G\right\}\right|$$
64		fvex	$$⊢0_G\in \mathrm{V}$$
65		hashsng	$$⊢0_G\in \mathrm{V}\to \left|\left\{0_G\right\}\right|=1$$
66	64 65	ax-mp	$$⊢\left|\left\{0_G\right\}\right|=1$$
67	63 66	eqtrdi	$$⊢\phi \to \left|G\mathrm{DProd}\varnothing \right|=1$$
68	67	breq2d	$$⊢\phi \to \left(P\parallel \left|G\mathrm{DProd}\varnothing \right|\leftrightarrow P\parallel 1\right)$$
69	57 68	mtbird	$$⊢\phi \to \neg P\parallel \left|G\mathrm{DProd}\varnothing \right|$$
70	69	a1d	$$⊢\phi \to \left(\varnothing \subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\varnothing \right|\right)$$
71		ssun1	$$⊢z\subseteq z\cup \left\{q\right\}$$
72		sstr	$$⊢\left(z\subseteq z\cup \left\{q\right\}\wedge z\cup \left\{q\right\}\subseteq A\right)\to z\subseteq A$$
73	71 72	mpan	$$⊢z\cup \left\{q\right\}\subseteq A\to z\subseteq A$$
74	73	imim1i	$$⊢\left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)$$
75	9	simpld	$$⊢\phi \to G\mathrm{dom}\mathrm{DProd}T$$
76	75 10	dprdf2	$$⊢\phi \to T:A⟶\mathrm{SubGrp}\left(G\right)$$
77	76	adantr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to T:A⟶\mathrm{SubGrp}\left(G\right)$$
78		simprr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to z\cup \left\{q\right\}\subseteq A$$
79	78	ssdifssd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\subseteq A$$
80	77 79	fssresd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right):\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}⟶\mathrm{SubGrp}\left(G\right)$$
81		simprl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \neg q\in z$$
82		disjsn	$$⊢z\cap \left\{q\right\}=\varnothing \leftrightarrow \neg q\in z$$
83	81 82	sylibr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to z\cap \left\{q\right\}=\varnothing$$
84	83	difeq1d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(z\cap \left\{q\right\}\right)\setminus \left\{P\right\}=\varnothing \setminus \left\{P\right\}$$
85		difindir	$$⊢\left(z\cap \left\{q\right\}\right)\setminus \left\{P\right\}=\left(z\setminus \left\{P\right\}\right)\cap \left(\left\{q\right\}\setminus \left\{P\right\}\right)$$
86	84 85 18	3eqtr3g	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(z\setminus \left\{P\right\}\right)\cap \left(\left\{q\right\}\setminus \left\{P\right\}\right)=\varnothing$$
87		difundir	$$⊢\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}=\left(z\setminus \left\{P\right\}\right)\cup \left(\left\{q\right\}\setminus \left\{P\right\}\right)$$
88	87	a1i	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}=\left(z\setminus \left\{P\right\}\right)\cup \left(\left\{q\right\}\setminus \left\{P\right\}\right)$$
89		eqid	$$⊢\mathrm{LSSum}\left(G\right)=\mathrm{LSSum}\left(G\right)$$
90	75	adantr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{dom}\mathrm{DProd}T$$
91	10	adantr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \mathrm{dom}T=A$$
92	90 91 79	dprdres	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(G\mathrm{dom}\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\wedge G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\subseteq G\mathrm{DProd}T\right)$$
93	92	simpld	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{dom}\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)$$
94	80 86 88 89 93	dprdsplit	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)=\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right)\mathrm{LSSum}\left(G\right)\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right)$$
95	94	fveq2d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|=\left|\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right)\mathrm{LSSum}\left(G\right)\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right)\right|$$
96		eqid	$$⊢\mathrm{Cntz}\left(G\right)=\mathrm{Cntz}\left(G\right)$$
97	80	fdmd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \mathrm{dom}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)=\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}$$
98		ssdif	$$⊢z\subseteq z\cup \left\{q\right\}\to z\setminus \left\{P\right\}\subseteq \left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}$$
99	71 98	mp1i	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to z\setminus \left\{P\right\}\subseteq \left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}$$
100	93 97 99	dprdres	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(G\mathrm{dom}\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\wedge G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\subseteq G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right)$$
101	100	simpld	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{dom}\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)$$
102		dprdsubg	$$⊢G\mathrm{dom}\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
103	101 102	syl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
104		ssun2	$$⊢\left\{q\right\}\subseteq z\cup \left\{q\right\}$$
105		ssdif	$$⊢\left\{q\right\}\subseteq z\cup \left\{q\right\}\to \left\{q\right\}\setminus \left\{P\right\}\subseteq \left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}$$
106	104 105	mp1i	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left\{q\right\}\setminus \left\{P\right\}\subseteq \left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}$$
107	93 97 106	dprdres	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(G\mathrm{dom}\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\wedge G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\subseteq G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right)$$
108	107	simpld	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{dom}\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)$$
109		dprdsubg	$$⊢G\mathrm{dom}\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
110	108 109	syl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{SubGrp}\left(G\right)$$
111	93 97 99 106 86 59	dprddisj2	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right)\cap \left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right)=\left\{0_G\right\}$$
112	93 97 99 106 86 96	dprdcntz2	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\subseteq \mathrm{Cntz}\left(G\right)\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right)$$
113	5	adantr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to B\in \mathrm{Fin}$$
114	1	dprdssv	$$⊢G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\subseteq B$$
115		ssfi	$$⊢\left(B\in \mathrm{Fin}\wedge G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\subseteq B\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
116	113 114 115	sylancl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
117	1	dprdssv	$$⊢G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\subseteq B$$
118		ssfi	$$⊢\left(B\in \mathrm{Fin}\wedge G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\subseteq B\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
119	113 117 118	sylancl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
120	89 59 96 103 110 111 112 116 119	lsmhash	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right)\mathrm{LSSum}\left(G\right)\left(G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right)\right|=\left|G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
121	99	resabs1d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to {\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}$$
122	121	oveq2d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)$$
123	122	fveq2d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|$$
124	106	resabs1d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to {\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}$$
125	124	oveq2d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)$$
126	125	fveq2d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
127	123 126	oveq12d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
128	95 120 127	3eqtrd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|=\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
129	128	breq2d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\right)$$
130	13	adantr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to P\in \mathbb{P}$$
131	1	dprdssv	$$⊢G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\subseteq B$$
132		ssfi	$$⊢\left(B\in \mathrm{Fin}\wedge G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\subseteq B\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
133	113 131 132	sylancl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
134		hashcl	$$⊢G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\in {\mathbb{N}}_0$$
135	133 134	syl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\in {\mathbb{N}}_0$$
136	135	nn0zd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\in \mathbb{Z}$$
137	1	dprdssv	$$⊢G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\subseteq B$$
138		ssfi	$$⊢\left(B\in \mathrm{Fin}\wedge G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\subseteq B\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
139	113 137 138	sylancl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}$$
140		hashcl	$$⊢G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\in \mathrm{Fin}\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\in {\mathbb{N}}_0$$
141	139 140	syl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\in {\mathbb{N}}_0$$
142	141	nn0zd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\in \mathbb{Z}$$
143		euclemma	$$⊢\left(P\in \mathbb{P}\wedge \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\in \mathbb{Z}\wedge \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\in \mathbb{Z}\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\vee P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
144	130 136 142 143	syl3anc	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\vee P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
145	129 144	bitrd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\vee P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
146	57	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \neg P\parallel 1$$
147		simpr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to q=P$$
148	147	sneqd	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \left\{q\right\}=\left\{P\right\}$$
149	148	difeq1d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \left\{q\right\}\setminus \left\{P\right\}=\left\{P\right\}\setminus \left\{P\right\}$$
150		difid	$$⊢\left\{P\right\}\setminus \left\{P\right\}=\varnothing$$
151	149 150	eqtrdi	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \left\{q\right\}\setminus \left\{P\right\}=\varnothing$$
152	151	reseq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to {T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}={T\upharpoonright }_{\varnothing }$$
153	152 21	eqtrdi	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to {T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}=\varnothing$$
154	153	oveq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)=G\mathrm{DProd}\varnothing$$
155	62	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to G\mathrm{DProd}\varnothing =\left\{0_G\right\}$$
156	154 155	eqtrd	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)=\left\{0_G\right\}$$
157	156	fveq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|=\left|\left\{0_G\right\}\right|$$
158	157 66	eqtrdi	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|=1$$
159	158	breq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel 1\right)$$
160	146 159	mtbird	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q=P\right)\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
161	6	adantr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to A\subseteq \mathbb{P}$$
162	78	unssbd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left\{q\right\}\subseteq A$$
163		vex	$$⊢q\in \mathrm{V}$$
164	163	snss	$$⊢q\in A\leftrightarrow \left\{q\right\}\subseteq A$$
165	162 164	sylibr	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to q\in A$$
166	161 165	sseldd	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to q\in \mathbb{P}$$
167	165 11	syldan	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to C\in {\mathbb{N}}_0$$
168		prmdvdsexpr	$$⊢\left(P\in \mathbb{P}\wedge q\in \mathbb{P}\wedge C\in {\mathbb{N}}_0\right)\to \left(P\parallel q^C\to P=q\right)$$
169	130 166 167 168	syl3anc	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(P\parallel q^C\to P=q\right)$$
170		eqcom	$$⊢P=q\leftrightarrow q=P$$
171	169 170	imbitrdi	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(P\parallel q^C\to q=P\right)$$
172	171	necon3ad	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(q\ne P\to \neg P\parallel q^C\right)$$
173	172	imp	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \neg P\parallel q^C$$
174		disjsn2	$$⊢q\ne P\to \left\{q\right\}\cap \left\{P\right\}=\varnothing$$
175	174	adantl	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \left\{q\right\}\cap \left\{P\right\}=\varnothing$$
176		disj3	$$⊢\left\{q\right\}\cap \left\{P\right\}=\varnothing \leftrightarrow \left\{q\right\}=\left\{q\right\}\setminus \left\{P\right\}$$
177	175 176	sylib	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \left\{q\right\}=\left\{q\right\}\setminus \left\{P\right\}$$
178	177	reseq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to {T\upharpoonright }_{\left\{q\right\}}={T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}$$
179	178	oveq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left\{q\right\}}\right)=G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)$$
180	75	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to G\mathrm{dom}\mathrm{DProd}T$$
181	10	ad2antrr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \mathrm{dom}T=A$$
182	165	adantr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to q\in A$$
183	180 181 182	dpjlem	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left\{q\right\}}\right)=T\left(q\right)$$
184	179 183	eqtr3d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)=T\left(q\right)$$
185	184	fveq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|=\left|T\left(q\right)\right|$$
186	165 12	syldan	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left|T\left(q\right)\right|=q^C$$
187	186	adantr	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \left|T\left(q\right)\right|=q^C$$
188	185 187	eqtrd	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|=q^C$$
189	188	breq2d	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\leftrightarrow P\parallel q^C\right)$$
190	173 189	mtbird	$$⊢\left(\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\wedge q\ne P\right)\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
191	160 190	pm2.61dane	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|$$
192		orel2	$$⊢\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\to \left(\left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\vee P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\right)\to P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)$$
193	191 192	syl	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(\left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\vee P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left\{q\right\}\setminus \left\{P\right\}\right)}\right)\right|\right)\to P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)$$
194	145 193	sylbid	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\to P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)$$
195	194	con3d	$$⊢\left(\phi \wedge \left(\neg q\in z\wedge z\cup \left\{q\right\}\subseteq A\right)\right)\to \left(\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)$$
196	195	expr	$$⊢\left(\phi \wedge \neg q\in z\right)\to \left(z\cup \left\{q\right\}\subseteq A\to \left(\neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
197	196	a2d	$$⊢\left(\phi \wedge \neg q\in z\right)\to \left(\left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
198	74 197	syl5	$$⊢\left(\phi \wedge \neg q\in z\right)\to \left(\left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
199	198	expcom	$$⊢\neg q\in z\to \left(\phi \to \left(\left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\right)$$
200	199	adantl	$$⊢\left(z\in \mathrm{Fin}\wedge \neg q\in z\right)\to \left(\phi \to \left(\left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\right)$$
201	200	a2d	$$⊢\left(z\in \mathrm{Fin}\wedge \neg q\in z\right)\to \left(\left(\phi \to \left(z\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(z\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\to \left(\phi \to \left(z\cup \left\{q\right\}\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(\left(z\cup \left\{q\right\}\right)\setminus \left\{P\right\}\right)}\right)\right|\right)\right)\right)$$
202	28 37 46 55 70 201	findcard2s	$$⊢A\in \mathrm{Fin}\to \left(\phi \to \left(A\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|\right)\right)$$
203	14 202	mpcom	$$⊢\phi \to \left(A\subseteq A\to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|\right)$$
204	15 203	mpi	$$⊢\phi \to \neg P\parallel \left|G\mathrm{DProd}\left({T\upharpoonright }_{\left(A\setminus \left\{P\right\}\right)}\right)\right|$$