ablfac1eu

Description: The factorization of ablfac1b is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to S . (Contributed by Mario Carneiro, 21-Apr-2016)

	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}$
Assertion	ablfac1eu	$⊢ φ \to T = S$

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	9	simpld	$⊢ φ \to G dom DProd T$
14	13 10	dprdf2	$⊢ φ \to T : A ⟶ SubGrp (G)$
15	14	ffnd	$⊢ φ \to T Fn A$
16	1 2 3 4 5 6	ablfac1b	$⊢ φ \to G dom DProd S$
17	1	fvexi	$⊢ B \in V$
18	17	rabex	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in V$
19	18 3	dmmpti	$⊢ dom S = A$
20	19	a1i	$⊢ φ \to dom S = A$
21	16 20	dprdf2	$⊢ φ \to S : A ⟶ SubGrp (G)$
22	21	ffnd	$⊢ φ \to S Fn A$
23	5	adantr	$⊢ (φ \land q \in A) \to B \in Fin$
24	21	ffvelrnda	$⊢ (φ \land q \in A) \to S (q) \in SubGrp (G)$
25	1	subgss	$⊢ S (q) \in SubGrp (G) \to S (q) \subseteq B$
26	24 25	syl	$⊢ (φ \land q \in A) \to S (q) \subseteq B$
27	23 26	ssfid	$⊢ (φ \land q \in A) \to S (q) \in Fin$
28	14	ffvelrnda	$⊢ (φ \land q \in A) \to T (q) \in SubGrp (G)$
29	1	subgss	$⊢ T (q) \in SubGrp (G) \to T (q) \subseteq B$
30	28 29	syl	$⊢ (φ \land q \in A) \to T (q) \subseteq B$
31	30	sselda	$⊢ ((φ \land q \in A) \land x \in T (q)) \to x \in B$
32	1 2	odcl	$⊢ x \in B \to O (x) \in ℕ_{0}$
33	31 32	syl	$⊢ ((φ \land q \in A) \land x \in T (q)) \to O (x) \in ℕ_{0}$
34	33	nn0zd	$⊢ ((φ \land q \in A) \land x \in T (q)) \to O (x) \in ℤ$
35	23 30	ssfid	$⊢ (φ \land q \in A) \to T (q) \in Fin$
36		hashcl	$⊢ T (q) \in Fin \to \|T (q)\| \in ℕ_{0}$
37	35 36	syl	$⊢ (φ \land q \in A) \to \|T (q)\| \in ℕ_{0}$
38	37	nn0zd	$⊢ (φ \land q \in A) \to \|T (q)\| \in ℤ$
39	38	adantr	$⊢ ((φ \land q \in A) \land x \in T (q)) \to \|T (q)\| \in ℤ$
40	6	sselda	$⊢ (φ \land q \in A) \to q \in ℙ$
41		prmnn	$⊢ q \in ℙ \to q \in ℕ$
42	40 41	syl	$⊢ (φ \land q \in A) \to q \in ℕ$
43		ablgrp	$⊢ G \in Abel \to G \in Grp$
44	4 43	syl	$⊢ φ \to G \in Grp$
45	1	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
46	44 45	syl	$⊢ φ \to B \neq \emptyset$
47		hashnncl	$⊢ B \in Fin \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
48	5 47	syl	$⊢ φ \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
49	46 48	mpbird	$⊢ φ \to \|B\| \in ℕ$
50	49	adantr	$⊢ (φ \land q \in A) \to \|B\| \in ℕ$
51	40 50	pccld	$⊢ (φ \land q \in A) \to q pCnt \|B\| \in ℕ_{0}$
52	42 51	nnexpcld	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} \in ℕ$
53	52	nnzd	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} \in ℤ$
54	53	adantr	$⊢ ((φ \land q \in A) \land x \in T (q)) \to q^{q pCnt \|B\|} \in ℤ$
55	28	adantr	$⊢ ((φ \land q \in A) \land x \in T (q)) \to T (q) \in SubGrp (G)$
56	35	adantr	$⊢ ((φ \land q \in A) \land x \in T (q)) \to T (q) \in Fin$
57		simpr	$⊢ ((φ \land q \in A) \land x \in T (q)) \to x \in T (q)$
58	2	odsubdvds	$⊢ (T (q) \in SubGrp (G) \land T (q) \in Fin \land x \in T (q)) \to O (x) ∥ \|T (q)\|$
59	55 56 57 58	syl3anc	$⊢ ((φ \land q \in A) \land x \in T (q)) \to O (x) ∥ \|T (q)\|$
60		prmz	$⊢ q \in ℙ \to q \in ℤ$
61	40 60	syl	$⊢ (φ \land q \in A) \to q \in ℤ$
62	11	nn0zd	$⊢ (φ \land q \in A) \to C \in ℤ$
63	51	nn0zd	$⊢ (φ \land q \in A) \to q pCnt \|B\| \in ℤ$
64	1	lagsubg	$⊢ (T (q) \in SubGrp (G) \land B \in Fin) \to \|T (q)\| ∥ \|B\|$
65	28 23 64	syl2anc	$⊢ (φ \land q \in A) \to \|T (q)\| ∥ \|B\|$
66	12 65	eqbrtrrd	$⊢ (φ \land q \in A) \to q^{C} ∥ \|B\|$
67	50	nnzd	$⊢ (φ \land q \in A) \to \|B\| \in ℤ$
68		pcdvdsb	$⊢ (q \in ℙ \land \|B\| \in ℤ \land C \in ℕ_{0}) \to (C \leq q pCnt \|B\| \leftrightarrow q^{C} ∥ \|B\|)$
69	40 67 11 68	syl3anc	$⊢ (φ \land q \in A) \to (C \leq q pCnt \|B\| \leftrightarrow q^{C} ∥ \|B\|)$
70	66 69	mpbird	$⊢ (φ \land q \in A) \to C \leq q pCnt \|B\|$
71		eluz2	$⊢ q pCnt \|B\| \in ℤ_{\geq C} \leftrightarrow (C \in ℤ \land q pCnt \|B\| \in ℤ \land C \leq q pCnt \|B\|)$
72	62 63 70 71	syl3anbrc	$⊢ (φ \land q \in A) \to q pCnt \|B\| \in ℤ_{\geq C}$
73		dvdsexp	$⊢ (q \in ℤ \land C \in ℕ_{0} \land q pCnt \|B\| \in ℤ_{\geq C}) \to q^{C} ∥ q^{q pCnt \|B\|}$
74	61 11 72 73	syl3anc	$⊢ (φ \land q \in A) \to q^{C} ∥ q^{q pCnt \|B\|}$
75	12 74	eqbrtrd	$⊢ (φ \land q \in A) \to \|T (q)\| ∥ q^{q pCnt \|B\|}$
76	75	adantr	$⊢ ((φ \land q \in A) \land x \in T (q)) \to \|T (q)\| ∥ q^{q pCnt \|B\|}$
77	34 39 54 59 76	dvdstrd	$⊢ ((φ \land q \in A) \land x \in T (q)) \to O (x) ∥ q^{q pCnt \|B\|}$
78	30 77	ssrabdv	$⊢ (φ \land q \in A) \to T (q) \subseteq \{x \in B \| O (x) ∥ q^{q pCnt \|B\|}\}$
79		id	$⊢ p = q \to p = q$
80		oveq1	$⊢ p = q \to p pCnt \|B\| = q pCnt \|B\|$
81	79 80	oveq12d	$⊢ p = q \to p^{p pCnt \|B\|} = q^{q pCnt \|B\|}$
82	81	breq2d	$⊢ p = q \to (O (x) ∥ p^{p pCnt \|B\|} \leftrightarrow O (x) ∥ q^{q pCnt \|B\|})$
83	82	rabbidv	$⊢ p = q \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} = \{x \in B \| O (x) ∥ q^{q pCnt \|B\|}\}$
84	83 3 18	fvmpt3i	$⊢ q \in A \to S (q) = \{x \in B \| O (x) ∥ q^{q pCnt \|B\|}\}$
85	84	adantl	$⊢ (φ \land q \in A) \to S (q) = \{x \in B \| O (x) ∥ q^{q pCnt \|B\|}\}$
86	78 85	sseqtrrd	$⊢ (φ \land q \in A) \to T (q) \subseteq S (q)$
87	52	nnnn0d	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} \in ℕ_{0}$
88		pcdvds	$⊢ (q \in ℙ \land \|B\| \in ℕ) \to q^{q pCnt \|B\|} ∥ \|B\|$
89	40 50 88	syl2anc	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} ∥ \|B\|$
90	13	adantr	$⊢ (φ \land q \in A) \to G dom DProd T$
91	10	adantr	$⊢ (φ \land q \in A) \to dom T = A$
92	8	adantr	$⊢ (φ \land q \in A) \to D \subseteq A$
93	90 91 92	dprdres	$⊢ (φ \land q \in A) \to (G dom DProd ({T ↾}_{D}) \land G DProd ({T ↾}_{D}) \subseteq G DProd T)$
94	93	simpld	$⊢ (φ \land q \in A) \to G dom DProd ({T ↾}_{D})$
95	14	adantr	$⊢ (φ \land q \in A) \to T : A ⟶ SubGrp (G)$
96	95 92	fssresd	$⊢ (φ \land q \in A) \to ({T ↾}_{D}) : D ⟶ SubGrp (G)$
97	96	fdmd	$⊢ (φ \land q \in A) \to dom ({T ↾}_{D}) = D$
98		difssd	$⊢ (φ \land q \in A) \to D ∖ \{q\} \subseteq D$
99	94 97 98	dprdres	$⊢ (φ \land q \in A) \to (G dom DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \land G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \subseteq G DProd ({T ↾}_{D}))$
100	99	simpld	$⊢ (φ \land q \in A) \to G dom DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})$
101		dprdsubg	$⊢ G dom DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \to G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in SubGrp (G)$
102	100 101	syl	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in SubGrp (G)$
103	1	lagsubg	$⊢ (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in SubGrp (G) \land B \in Fin) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|$
104	102 23 103	syl2anc	$⊢ (φ \land q \in A) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|$
105		eqid	$⊢ 0_{G} = 0_{G}$
106	105	subg0cl	$⊢ G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in SubGrp (G) \to 0_{G} \in (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}))$
107	102 106	syl	$⊢ (φ \land q \in A) \to 0_{G} \in (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}))$
108	107	ne0d	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \neq \emptyset$
109	1	dprdssv	$⊢ G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \subseteq B$
110		ssfi	$⊢ (B \in Fin \land G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \subseteq B) \to G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in Fin$
111	23 109 110	sylancl	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in Fin$
112		hashnncl	$⊢ G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \in Fin \to (\|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℕ \leftrightarrow G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \neq \emptyset)$
113	111 112	syl	$⊢ (φ \land q \in A) \to (\|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℕ \leftrightarrow G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}) \neq \emptyset)$
114	108 113	mpbird	$⊢ (φ \land q \in A) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℕ$
115	114	nnzd	$⊢ (φ \land q \in A) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℤ$
116		id	$⊢ x = q \to x = q$
117		sneq	$⊢ x = q \to \{x\} = \{q\}$
118	117	difeq2d	$⊢ x = q \to D ∖ \{x\} = D ∖ \{q\}$
119	118	reseq2d	$⊢ x = q \to {({T ↾}_{D}) ↾}_{(D ∖ \{x\})} = {({T ↾}_{D}) ↾}_{(D ∖ \{q\})}$
120	119	oveq2d	$⊢ x = q \to G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})}) = G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})$
121	120	fveq2d	$⊢ x = q \to \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})})\| = \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|$
122	116 121	breq12d	$⊢ x = q \to (x ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})})\| \leftrightarrow q ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|)$
123	122	notbid	$⊢ x = q \to (\neg x ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})})\| \leftrightarrow \neg q ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|)$
124		eqid	$⊢ (p \in D ⟼ \{y \in B \| O (y) ∥ p^{p pCnt \|B\|}\}) = (p \in D ⟼ \{y \in B \| O (y) ∥ p^{p pCnt \|B\|}\})$
125	4	adantr	$⊢ (φ \land x \in ℙ) \to G \in Abel$
126	5	adantr	$⊢ (φ \land x \in ℙ) \to B \in Fin$
127	7	ssrab3	$⊢ D \subseteq ℙ$
128	127	a1i	$⊢ (φ \land x \in ℙ) \to D \subseteq ℙ$
129		ssidd	$⊢ (φ \land x \in ℙ) \to D \subseteq D$
130	13 10 8	dprdres	$⊢ φ \to (G dom DProd ({T ↾}_{D}) \land G DProd ({T ↾}_{D}) \subseteq G DProd T)$
131	130	simpld	$⊢ φ \to G dom DProd ({T ↾}_{D})$
132		dprdsubg	$⊢ G dom DProd ({T ↾}_{D}) \to G DProd ({T ↾}_{D}) \in SubGrp (G)$
133	131 132	syl	$⊢ φ \to G DProd ({T ↾}_{D}) \in SubGrp (G)$
134		difssd	$⊢ φ \to A ∖ D \subseteq A$
135	13 10 134	dprdres	$⊢ φ \to (G dom DProd ({T ↾}_{(A ∖ D)}) \land G DProd ({T ↾}_{(A ∖ D)}) \subseteq G DProd T)$
136	135	simpld	$⊢ φ \to G dom DProd ({T ↾}_{(A ∖ D)})$
137		dprdsubg	$⊢ G dom DProd ({T ↾}_{(A ∖ D)}) \to G DProd ({T ↾}_{(A ∖ D)}) \in SubGrp (G)$
138	136 137	syl	$⊢ φ \to G DProd ({T ↾}_{(A ∖ D)}) \in SubGrp (G)$
139		difss	$⊢ A ∖ D \subseteq A$
140		fssres	$⊢ (T : A ⟶ SubGrp (G) \land A ∖ D \subseteq A) \to ({T ↾}_{(A ∖ D)}) : A ∖ D ⟶ SubGrp (G)$
141	14 139 140	sylancl	$⊢ φ \to ({T ↾}_{(A ∖ D)}) : A ∖ D ⟶ SubGrp (G)$
142	141	fdmd	$⊢ φ \to dom ({T ↾}_{(A ∖ D)}) = A ∖ D$
143		fvres	$⊢ q \in (A ∖ D) \to ({T ↾}_{(A ∖ D)}) (q) = T (q)$
144	143	adantl	$⊢ (φ \land q \in (A ∖ D)) \to ({T ↾}_{(A ∖ D)}) (q) = T (q)$
145		eldif	$⊢ q \in (A ∖ D) \leftrightarrow (q \in A \land \neg q \in D)$
146	35	adantrr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to T (q) \in Fin$
147	105	subg0cl	$⊢ T (q) \in SubGrp (G) \to 0_{G} \in T (q)$
148	28 147	syl	$⊢ (φ \land q \in A) \to 0_{G} \in T (q)$
149	148	snssd	$⊢ (φ \land q \in A) \to \{0_{G}\} \subseteq T (q)$
150	149	adantrr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \{0_{G}\} \subseteq T (q)$
151		fvex	$⊢ 0_{G} \in V$
152		hashsng	$⊢ 0_{G} \in V \to \|\{0_{G}\}\| = 1$
153	151 152	ax-mp	$⊢ \|\{0_{G}\}\| = 1$
154	12	adantrr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \|T (q)\| = q^{C}$
155	40	adantr	$⊢ ((φ \land q \in A) \land C \in ℕ) \to q \in ℙ$
156		iddvdsexp	$⊢ (q \in ℤ \land C \in ℕ) \to q ∥ q^{C}$
157	61 156	sylan	$⊢ ((φ \land q \in A) \land C \in ℕ) \to q ∥ q^{C}$
158	66	adantr	$⊢ ((φ \land q \in A) \land C \in ℕ) \to q^{C} ∥ \|B\|$
159	12 38	eqeltrrd	$⊢ (φ \land q \in A) \to q^{C} \in ℤ$
160		dvdstr	$⊢ (q \in ℤ \land q^{C} \in ℤ \land \|B\| \in ℤ) \to ((q ∥ q^{C} \land q^{C} ∥ \|B\|) \to q ∥ \|B\|)$
161	61 159 67 160	syl3anc	$⊢ (φ \land q \in A) \to ((q ∥ q^{C} \land q^{C} ∥ \|B\|) \to q ∥ \|B\|)$
162	161	adantr	$⊢ ((φ \land q \in A) \land C \in ℕ) \to ((q ∥ q^{C} \land q^{C} ∥ \|B\|) \to q ∥ \|B\|)$
163	157 158 162	mp2and	$⊢ ((φ \land q \in A) \land C \in ℕ) \to q ∥ \|B\|$
164		breq1	$⊢ w = q \to (w ∥ \|B\| \leftrightarrow q ∥ \|B\|)$
165	164 7	elrab2	$⊢ q \in D \leftrightarrow (q \in ℙ \land q ∥ \|B\|)$
166	155 163 165	sylanbrc	$⊢ ((φ \land q \in A) \land C \in ℕ) \to q \in D$
167	166	ex	$⊢ (φ \land q \in A) \to (C \in ℕ \to q \in D)$
168	167	con3d	$⊢ (φ \land q \in A) \to (\neg q \in D \to \neg C \in ℕ)$
169	168	impr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \neg C \in ℕ$
170	11	adantrr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to C \in ℕ_{0}$
171		elnn0	$⊢ C \in ℕ_{0} \leftrightarrow (C \in ℕ \lor C = 0)$
172	170 171	sylib	$⊢ (φ \land (q \in A \land \neg q \in D)) \to (C \in ℕ \lor C = 0)$
173	172	ord	$⊢ (φ \land (q \in A \land \neg q \in D)) \to (\neg C \in ℕ \to C = 0)$
174	169 173	mpd	$⊢ (φ \land (q \in A \land \neg q \in D)) \to C = 0$
175	174	oveq2d	$⊢ (φ \land (q \in A \land \neg q \in D)) \to q^{C} = q^{0}$
176	42	adantrr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to q \in ℕ$
177	176	nncnd	$⊢ (φ \land (q \in A \land \neg q \in D)) \to q \in ℂ$
178	177	exp0d	$⊢ (φ \land (q \in A \land \neg q \in D)) \to q^{0} = 1$
179	154 175 178	3eqtrd	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \|T (q)\| = 1$
180	153 179	eqtr4id	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \|\{0_{G}\}\| = \|T (q)\|$
181		snfi	$⊢ \{0_{G}\} \in Fin$
182		hashen	$⊢ (\{0_{G}\} \in Fin \land T (q) \in Fin) \to (\|\{0_{G}\}\| = \|T (q)\| \leftrightarrow \{0_{G}\} \approx T (q))$
183	181 146 182	sylancr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to (\|\{0_{G}\}\| = \|T (q)\| \leftrightarrow \{0_{G}\} \approx T (q))$
184	180 183	mpbid	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \{0_{G}\} \approx T (q)$
185		fisseneq	$⊢ (T (q) \in Fin \land \{0_{G}\} \subseteq T (q) \land \{0_{G}\} \approx T (q)) \to \{0_{G}\} = T (q)$
186	146 150 184 185	syl3anc	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \{0_{G}\} = T (q)$
187	105	subg0cl	$⊢ G DProd ({T ↾}_{D}) \in SubGrp (G) \to 0_{G} \in (G DProd ({T ↾}_{D}))$
188	133 187	syl	$⊢ φ \to 0_{G} \in (G DProd ({T ↾}_{D}))$
189	188	adantr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to 0_{G} \in (G DProd ({T ↾}_{D}))$
190	189	snssd	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \{0_{G}\} \subseteq G DProd ({T ↾}_{D})$
191	186 190	eqsstrrd	$⊢ (φ \land (q \in A \land \neg q \in D)) \to T (q) \subseteq G DProd ({T ↾}_{D})$
192	145 191	sylan2b	$⊢ (φ \land q \in (A ∖ D)) \to T (q) \subseteq G DProd ({T ↾}_{D})$
193	144 192	eqsstrd	$⊢ (φ \land q \in (A ∖ D)) \to ({T ↾}_{(A ∖ D)}) (q) \subseteq G DProd ({T ↾}_{D})$
194	136 142 133 193	dprdlub	$⊢ φ \to G DProd ({T ↾}_{(A ∖ D)}) \subseteq G DProd ({T ↾}_{D})$
195		eqid	$⊢ LSSum (G) = LSSum (G)$
196	195	lsmss2	$⊢ (G DProd ({T ↾}_{D}) \in SubGrp (G) \land G DProd ({T ↾}_{(A ∖ D)}) \in SubGrp (G) \land G DProd ({T ↾}_{(A ∖ D)}) \subseteq G DProd ({T ↾}_{D})) \to (G DProd ({T ↾}_{D})) LSSum (G) (G DProd ({T ↾}_{(A ∖ D)})) = G DProd ({T ↾}_{D})$
197	133 138 194 196	syl3anc	$⊢ φ \to (G DProd ({T ↾}_{D})) LSSum (G) (G DProd ({T ↾}_{(A ∖ D)})) = G DProd ({T ↾}_{D})$
198		disjdif	$⊢ D \cap (A ∖ D) = \emptyset$
199	198	a1i	$⊢ φ \to D \cap (A ∖ D) = \emptyset$
200		undif2	$⊢ D \cup (A ∖ D) = D \cup A$
201		ssequn1	$⊢ D \subseteq A \leftrightarrow D \cup A = A$
202	8 201	sylib	$⊢ φ \to D \cup A = A$
203	200 202	syl5req	$⊢ φ \to A = D \cup (A ∖ D)$
204	14 199 203 195 13	dprdsplit	$⊢ φ \to G DProd T = (G DProd ({T ↾}_{D})) LSSum (G) (G DProd ({T ↾}_{(A ∖ D)}))$
205	9	simprd	$⊢ φ \to G DProd T = B$
206	204 205	eqtr3d	$⊢ φ \to (G DProd ({T ↾}_{D})) LSSum (G) (G DProd ({T ↾}_{(A ∖ D)})) = B$
207	197 206	eqtr3d	$⊢ φ \to G DProd ({T ↾}_{D}) = B$
208	131 207	jca	$⊢ φ \to (G dom DProd ({T ↾}_{D}) \land G DProd ({T ↾}_{D}) = B)$
209	208	adantr	$⊢ (φ \land x \in ℙ) \to (G dom DProd ({T ↾}_{D}) \land G DProd ({T ↾}_{D}) = B)$
210	14 8	fssresd	$⊢ φ \to ({T ↾}_{D}) : D ⟶ SubGrp (G)$
211	210	fdmd	$⊢ φ \to dom ({T ↾}_{D}) = D$
212	211	adantr	$⊢ (φ \land x \in ℙ) \to dom ({T ↾}_{D}) = D$
213	8	sselda	$⊢ (φ \land q \in D) \to q \in A$
214	213 11	syldan	$⊢ (φ \land q \in D) \to C \in ℕ_{0}$
215	214	adantlr	$⊢ ((φ \land x \in ℙ) \land q \in D) \to C \in ℕ_{0}$
216		fvres	$⊢ q \in D \to ({T ↾}_{D}) (q) = T (q)$
217	216	adantl	$⊢ (φ \land q \in D) \to ({T ↾}_{D}) (q) = T (q)$
218	217	fveq2d	$⊢ (φ \land q \in D) \to \|({T ↾}_{D}) (q)\| = \|T (q)\|$
219	213 12	syldan	$⊢ (φ \land q \in D) \to \|T (q)\| = q^{C}$
220	218 219	eqtrd	$⊢ (φ \land q \in D) \to \|({T ↾}_{D}) (q)\| = q^{C}$
221	220	adantlr	$⊢ ((φ \land x \in ℙ) \land q \in D) \to \|({T ↾}_{D}) (q)\| = q^{C}$
222		simpr	$⊢ (φ \land x \in ℙ) \to x \in ℙ$
223		fzfid	$⊢ φ \to (1 \dots \|B\|) \in Fin$
224		prmnn	$⊢ w \in ℙ \to w \in ℕ$
225	224	3ad2ant2	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to w \in ℕ$
226		prmz	$⊢ w \in ℙ \to w \in ℤ$
227		dvdsle	$⊢ (w \in ℤ \land \|B\| \in ℕ) \to (w ∥ \|B\| \to w \leq \|B\|)$
228	226 49 227	syl2anr	$⊢ (φ \land w \in ℙ) \to (w ∥ \|B\| \to w \leq \|B\|)$
229	228	3impia	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to w \leq \|B\|$
230	49	nnzd	$⊢ φ \to \|B\| \in ℤ$
231	230	3ad2ant1	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to \|B\| \in ℤ$
232		fznn	$⊢ \|B\| \in ℤ \to (w \in (1 \dots \|B\|) \leftrightarrow (w \in ℕ \land w \leq \|B\|))$
233	231 232	syl	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to (w \in (1 \dots \|B\|) \leftrightarrow (w \in ℕ \land w \leq \|B\|))$
234	225 229 233	mpbir2and	$⊢ (φ \land w \in ℙ \land w ∥ \|B\|) \to w \in (1 \dots \|B\|)$
235	234	rabssdv	$⊢ φ \to \{w \in ℙ \| w ∥ \|B\|\} \subseteq (1 \dots \|B\|)$
236	7 235	eqsstrid	$⊢ φ \to D \subseteq (1 \dots \|B\|)$
237	223 236	ssfid	$⊢ φ \to D \in Fin$
238	237	adantr	$⊢ (φ \land x \in ℙ) \to D \in Fin$
239	1 2 124 125 126 128 7 129 209 212 215 221 222 238	ablfac1eulem	$⊢ (φ \land x \in ℙ) \to \neg x ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})})\|$
240	239	ralrimiva	$⊢ φ \to \forall x \in ℙ \neg x ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})})\|$
241	240	adantr	$⊢ (φ \land q \in A) \to \forall x \in ℙ \neg x ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{x\})})\|$
242	123 241 40	rspcdva	$⊢ (φ \land q \in A) \to \neg q ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|$
243		coprm	$⊢ (q \in ℙ \land \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℤ) \to (\neg q ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \leftrightarrow q \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1)$
244	40 115 243	syl2anc	$⊢ (φ \land q \in A) \to (\neg q ∥ \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \leftrightarrow q \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1)$
245	242 244	mpbid	$⊢ (φ \land q \in A) \to q \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1$
246		rpexp1i	$⊢ (q \in ℤ \land \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℤ \land q pCnt \|B\| \in ℕ_{0}) \to (q \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1 \to q^{q pCnt \|B\|} \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1)$
247	61 115 51 246	syl3anc	$⊢ (φ \land q \in A) \to (q \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1 \to q^{q pCnt \|B\|} \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1)$
248	245 247	mpd	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1$
249		coprmdvds2	$⊢ ((q^{q pCnt \|B\|} \in ℤ \land \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℤ \land \|B\| \in ℤ) \land q^{q pCnt \|B\|} \gcd \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = 1) \to ((q^{q pCnt \|B\|} ∥ \|B\| \land \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|) \to q^{q pCnt \|B\|} \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|)$
250	53 115 67 248 249	syl31anc	$⊢ (φ \land q \in A) \to ((q^{q pCnt \|B\|} ∥ \|B\| \land \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|) \to q^{q pCnt \|B\|} \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|)$
251	89 104 250	mp2and	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|B\|$
252		eqid	$⊢ Cntz (G) = Cntz (G)$
253		inss1	$⊢ D \cap \{q\} \subseteq D$
254	253	a1i	$⊢ (φ \land q \in A) \to D \cap \{q\} \subseteq D$
255	94 97 254	dprdres	$⊢ (φ \land q \in A) \to (G dom DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \land G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \subseteq G DProd ({T ↾}_{D}))$
256	255	simpld	$⊢ (φ \land q \in A) \to G dom DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})$
257		dprdsubg	$⊢ G dom DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \in SubGrp (G)$
258	256 257	syl	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \in SubGrp (G)$
259		inass	$⊢ (D \cap \{q\}) \cap (D ∖ \{q\}) = D \cap (\{q\} \cap (D ∖ \{q\}))$
260		disjdif	$⊢ \{q\} \cap (D ∖ \{q\}) = \emptyset$
261	260	ineq2i	$⊢ D \cap (\{q\} \cap (D ∖ \{q\})) = D \cap \emptyset$
262		in0	$⊢ D \cap \emptyset = \emptyset$
263	259 261 262	3eqtri	$⊢ (D \cap \{q\}) \cap (D ∖ \{q\}) = \emptyset$
264	263	a1i	$⊢ (φ \land q \in A) \to (D \cap \{q\}) \cap (D ∖ \{q\}) = \emptyset$
265	94 97 254 98 264 105	dprddisj2	$⊢ (φ \land q \in A) \to (G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})) \cap (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})) = \{0_{G}\}$
266	94 97 254 98 264 252	dprdcntz2	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \subseteq Cntz (G) (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}))$
267	1	dprdssv	$⊢ G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \subseteq B$
268		ssfi	$⊢ (B \in Fin \land G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \subseteq B) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \in Fin$
269	23 267 268	sylancl	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) \in Fin$
270	195 105 252 258 102 265 266 269 111	lsmhash	$⊢ (φ \land q \in A) \to \|(G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})) LSSum (G) (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}))\| = \|G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|$
271		inundif	$⊢ (D \cap \{q\}) \cup (D ∖ \{q\}) = D$
272	271	eqcomi	$⊢ D = (D \cap \{q\}) \cup (D ∖ \{q\})$
273	272	a1i	$⊢ (φ \land q \in A) \to D = (D \cap \{q\}) \cup (D ∖ \{q\})$
274	96 264 273 195 94	dprdsplit	$⊢ (φ \land q \in A) \to G DProd ({T ↾}_{D}) = (G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})) LSSum (G) (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}))$
275	207	adantr	$⊢ (φ \land q \in A) \to G DProd ({T ↾}_{D}) = B$
276	274 275	eqtr3d	$⊢ (φ \land q \in A) \to (G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})) LSSum (G) (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})) = B$
277	276	fveq2d	$⊢ (φ \land q \in A) \to \|(G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})) LSSum (G) (G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})}))\| = \|B\|$
278		snssi	$⊢ q \in D \to \{q\} \subseteq D$
279	278	adantl	$⊢ ((φ \land q \in A) \land q \in D) \to \{q\} \subseteq D$
280		sseqin2	$⊢ \{q\} \subseteq D \leftrightarrow D \cap \{q\} = \{q\}$
281	279 280	sylib	$⊢ ((φ \land q \in A) \land q \in D) \to D \cap \{q\} = \{q\}$
282	281	reseq2d	$⊢ ((φ \land q \in A) \land q \in D) \to {({T ↾}_{D}) ↾}_{(D \cap \{q\})} = {({T ↾}_{D}) ↾}_{\{q\}}$
283	282	oveq2d	$⊢ ((φ \land q \in A) \land q \in D) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) = G DProd ({({T ↾}_{D}) ↾}_{\{q\}})$
284	94	adantr	$⊢ ((φ \land q \in A) \land q \in D) \to G dom DProd ({T ↾}_{D})$
285	211	ad2antrr	$⊢ ((φ \land q \in A) \land q \in D) \to dom ({T ↾}_{D}) = D$
286		simpr	$⊢ ((φ \land q \in A) \land q \in D) \to q \in D$
287	284 285 286	dpjlem	$⊢ ((φ \land q \in A) \land q \in D) \to G DProd ({({T ↾}_{D}) ↾}_{\{q\}}) = ({T ↾}_{D}) (q)$
288	216	adantl	$⊢ ((φ \land q \in A) \land q \in D) \to ({T ↾}_{D}) (q) = T (q)$
289	283 287 288	3eqtrd	$⊢ ((φ \land q \in A) \land q \in D) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) = T (q)$
290		simprr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to \neg q \in D$
291		disjsn	$⊢ D \cap \{q\} = \emptyset \leftrightarrow \neg q \in D$
292	290 291	sylibr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to D \cap \{q\} = \emptyset$
293	292	reseq2d	$⊢ (φ \land (q \in A \land \neg q \in D)) \to {({T ↾}_{D}) ↾}_{(D \cap \{q\})} = {({T ↾}_{D}) ↾}_{\emptyset}$
294		res0	$⊢ {({T ↾}_{D}) ↾}_{\emptyset} = \emptyset$
295	293 294	eqtrdi	$⊢ (φ \land (q \in A \land \neg q \in D)) \to {({T ↾}_{D}) ↾}_{(D \cap \{q\})} = \emptyset$
296	295	oveq2d	$⊢ (φ \land (q \in A \land \neg q \in D)) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) = G DProd \emptyset$
297	105	dprd0	$⊢ G \in Grp \to (G dom DProd \emptyset \land G DProd \emptyset = \{0_{G}\})$
298	44 297	syl	$⊢ φ \to (G dom DProd \emptyset \land G DProd \emptyset = \{0_{G}\})$
299	298	simprd	$⊢ φ \to G DProd \emptyset = \{0_{G}\}$
300	299	adantr	$⊢ (φ \land (q \in A \land \neg q \in D)) \to G DProd \emptyset = \{0_{G}\}$
301	296 300 186	3eqtrd	$⊢ (φ \land (q \in A \land \neg q \in D)) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) = T (q)$
302	301	anassrs	$⊢ ((φ \land q \in A) \land \neg q \in D) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) = T (q)$
303	289 302	pm2.61dan	$⊢ (φ \land q \in A) \to G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})}) = T (q)$
304	303	fveq2d	$⊢ (φ \land q \in A) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})\| = \|T (q)\|$
305	304	oveq1d	$⊢ (φ \land q \in A) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D \cap \{q\})})\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| = \|T (q)\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|$
306	270 277 305	3eqtr3d	$⊢ (φ \land q \in A) \to \|B\| = \|T (q)\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|$
307	251 306	breqtrd	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|T (q)\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\|$
308	114	nnne0d	$⊢ (φ \land q \in A) \to \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \neq 0$
309		dvdsmulcr	$⊢ (q^{q pCnt \|B\|} \in ℤ \land \|T (q)\| \in ℤ \land (\|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \in ℤ \land \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \neq 0)) \to (q^{q pCnt \|B\|} \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|T (q)\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \leftrightarrow q^{q pCnt \|B\|} ∥ \|T (q)\|)$
310	53 38 115 308 309	syl112anc	$⊢ (φ \land q \in A) \to (q^{q pCnt \|B\|} \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| ∥ \|T (q)\| \|G DProd ({({T ↾}_{D}) ↾}_{(D ∖ \{q\})})\| \leftrightarrow q^{q pCnt \|B\|} ∥ \|T (q)\|)$
311	307 310	mpbid	$⊢ (φ \land q \in A) \to q^{q pCnt \|B\|} ∥ \|T (q)\|$
312		dvdseq	$⊢ ((\|T (q)\| \in ℕ_{0} \land q^{q pCnt \|B\|} \in ℕ_{0}) \land (\|T (q)\| ∥ q^{q pCnt \|B\|} \land q^{q pCnt \|B\|} ∥ \|T (q)\|)) \to \|T (q)\| = q^{q pCnt \|B\|}$
313	37 87 75 311 312	syl22anc	$⊢ (φ \land q \in A) \to \|T (q)\| = q^{q pCnt \|B\|}$
314	1 2 3 4 5 6	ablfac1a	$⊢ (φ \land q \in A) \to \|S (q)\| = q^{q pCnt \|B\|}$
315	313 314	eqtr4d	$⊢ (φ \land q \in A) \to \|T (q)\| = \|S (q)\|$
316		hashen	$⊢ (T (q) \in Fin \land S (q) \in Fin) \to (\|T (q)\| = \|S (q)\| \leftrightarrow T (q) \approx S (q))$
317	35 27 316	syl2anc	$⊢ (φ \land q \in A) \to (\|T (q)\| = \|S (q)\| \leftrightarrow T (q) \approx S (q))$
318	315 317	mpbid	$⊢ (φ \land q \in A) \to T (q) \approx S (q)$
319		fisseneq	$⊢ (S (q) \in Fin \land T (q) \subseteq S (q) \land T (q) \approx S (q)) \to T (q) = S (q)$
320	27 86 318 319	syl3anc	$⊢ (φ \land q \in A) \to T (q) = S (q)$
321	15 22 320	eqfnfvd	$⊢ φ \to T = S$

Metamath Proof Explorer

Theorem ablfac1eu

Proof