ablfac1eulem

	Ref	Expression
Hypotheses	ablfac1.b	$⊢ B = {Base}_{G}$
	ablfac1.o	$⊢ O = od (G)$
	ablfac1.s	$⊢ S = (p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
	ablfac1.g	$⊢ φ \to G \in Abel$
	ablfac1.f	$⊢ φ \to B \in Fin$
	ablfac1.1	$⊢ φ \to A \subseteq ℙ$
	ablfac1c.d	$⊢ D = \{w \in ℙ \| w ∥ \|B\|\}$
	ablfac1.2	$⊢ φ \to D \subseteq A$
	ablfac1eu.1	$⊢ φ \to (G dom DProd T \land G DProd T = B)$
	ablfac1eu.2	$⊢ φ \to dom T = A$
	ablfac1eu.3	$⊢ (φ \land q \in A) \to C \in ℕ_{0}$
	ablfac1eu.4	$⊢ (φ \land q \in A) \to \|T (q)\| = q^{C}$
	ablfac1eulem.1	$⊢ φ \to P \in ℙ$
	ablfac1eulem.2	$⊢ φ \to A \in Fin$
Assertion	ablfac1eulem	$⊢ φ \to \neg P ∥ \|G DProd ({T ↾}_{(A ∖ \{P\})})\|$

Proof

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

Metamath Proof Explorer

Theorem ablfac1eulem

Proof