ablfac1b

Description: Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (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 ℙ$
Assertion	ablfac1b	$⊢ φ \to G dom DProd 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		eqid	$⊢ Cntz (G) = Cntz (G)$
8		eqid	$⊢ 0_{G} = 0_{G}$
9		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
10		ablgrp	$⊢ G \in Abel \to G \in Grp$
11	4 10	syl	$⊢ φ \to G \in Grp$
12		prmex	$⊢ ℙ \in V$
13	12	ssex	$⊢ A \subseteq ℙ \to A \in V$
14	6 13	syl	$⊢ φ \to A \in V$
15	4	adantr	$⊢ (φ \land p \in A) \to G \in Abel$
16	6	sselda	$⊢ (φ \land p \in A) \to p \in ℙ$
17		prmnn	$⊢ p \in ℙ \to p \in ℕ$
18	16 17	syl	$⊢ (φ \land p \in A) \to p \in ℕ$
19	1	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
20	11 19	syl	$⊢ φ \to B \neq \emptyset$
21		hashnncl	$⊢ B \in Fin \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
22	5 21	syl	$⊢ φ \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
23	20 22	mpbird	$⊢ φ \to \|B\| \in ℕ$
24	23	adantr	$⊢ (φ \land p \in A) \to \|B\| \in ℕ$
25	16 24	pccld	$⊢ (φ \land p \in A) \to p pCnt \|B\| \in ℕ_{0}$
26	18 25	nnexpcld	$⊢ (φ \land p \in A) \to p^{p pCnt \|B\|} \in ℕ$
27	26	nnzd	$⊢ (φ \land p \in A) \to p^{p pCnt \|B\|} \in ℤ$
28	2 1	oddvdssubg	$⊢ (G \in Abel \land p^{p pCnt \|B\|} \in ℤ) \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in SubGrp (G)$
29	15 27 28	syl2anc	$⊢ (φ \land p \in A) \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in SubGrp (G)$
30	29 3	fmptd	$⊢ φ \to S : A ⟶ SubGrp (G)$
31	4	adantr	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to G \in Abel$
32	30	adantr	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to S : A ⟶ SubGrp (G)$
33		simpr1	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to a \in A$
34	32 33	ffvelcdmd	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to S (a) \in SubGrp (G)$
35		simpr2	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to b \in A$
36	32 35	ffvelcdmd	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to S (b) \in SubGrp (G)$
37	7 31 34 36	ablcntzd	$⊢ (φ \land (a \in A \land b \in A \land a \neq b)) \to S (a) \subseteq Cntz (G) (S (b))$
38		id	$⊢ p = a \to p = a$
39		oveq1	$⊢ p = a \to p pCnt \|B\| = a pCnt \|B\|$
40	38 39	oveq12d	$⊢ p = a \to p^{p pCnt \|B\|} = a^{a pCnt \|B\|}$
41	40	breq2d	$⊢ p = a \to (O (x) ∥ p^{p pCnt \|B\|} \leftrightarrow O (x) ∥ a^{a pCnt \|B\|})$
42	41	rabbidv	$⊢ p = a \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} = \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\}$
43	1	fvexi	$⊢ B \in V$
44	43	rabex	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in V$
45	42 3 44	fvmpt3i	$⊢ a \in A \to S (a) = \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\}$
46	45	adantl	$⊢ (φ \land a \in A) \to S (a) = \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\}$
47		eqimss	$⊢ S (a) = \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} \to S (a) \subseteq \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\}$
48	46 47	syl	$⊢ (φ \land a \in A) \to S (a) \subseteq \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\}$
49	4	adantr	$⊢ (φ \land a \in A) \to G \in Abel$
50		eqid	$⊢ {Base}_{G} = {Base}_{G}$
51	50	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
52		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
53	49 10 51 52	4syl	$⊢ (φ \land a \in A) \to SubGrp (G) \in Moore ({Base}_{G})$
54		df-ima	$⊢ S [A ∖ \{a\}] = ran ({S ↾}_{(A ∖ \{a\})})$
55	6	sselda	$⊢ (φ \land a \in A) \to a \in ℙ$
56	55	ad2antrr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a \in ℙ$
57	23	ad3antrrr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to \|B\| \in ℕ$
58		pcdvds	$⊢ (a \in ℙ \land \|B\| \in ℕ) \to a^{a pCnt \|B\|} ∥ \|B\|$
59	56 57 58	syl2anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} ∥ \|B\|$
60	6	ad3antrrr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to A \subseteq ℙ$
61		eldifi	$⊢ p \in (A ∖ \{a\}) \to p \in A$
62	61	ad2antlr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p \in A$
63	60 62	sseldd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p \in ℙ$
64		pcdvds	$⊢ (p \in ℙ \land \|B\| \in ℕ) \to p^{p pCnt \|B\|} ∥ \|B\|$
65	63 57 64	syl2anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p^{p pCnt \|B\|} ∥ \|B\|$
66		eqid	$⊢ a^{a pCnt \|B\|} = a^{a pCnt \|B\|}$
67		eqid	$⊢ \frac{\|B\|}{a^{a pCnt \|B\|}} = \frac{\|B\|}{a^{a pCnt \|B\|}}$
68	1 2 3 4 5 6 66 67	ablfac1lem	$⊢ (φ \land a \in A) \to ((a^{a pCnt \|B\|} \in ℕ \land \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℕ) \land a^{a pCnt \|B\|} \gcd (\frac{\|B\|}{a^{a pCnt \|B\|}}) = 1 \land \|B\| = a^{a pCnt \|B\|} (\frac{\|B\|}{a^{a pCnt \|B\|}}))$
69	68	simp1d	$⊢ (φ \land a \in A) \to (a^{a pCnt \|B\|} \in ℕ \land \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℕ)$
70	69	simpld	$⊢ (φ \land a \in A) \to a^{a pCnt \|B\|} \in ℕ$
71	70	ad2antrr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} \in ℕ$
72	71	nnzd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} \in ℤ$
73	63 17	syl	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p \in ℕ$
74	63 57	pccld	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p pCnt \|B\| \in ℕ_{0}$
75	73 74	nnexpcld	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p^{p pCnt \|B\|} \in ℕ$
76	75	nnzd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p^{p pCnt \|B\|} \in ℤ$
77	57	nnzd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to \|B\| \in ℤ$
78		eldifsni	$⊢ p \in (A ∖ \{a\}) \to p \neq a$
79	78	ad2antlr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p \neq a$
80	79	necomd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a \neq p$
81		prmrp	$⊢ (a \in ℙ \land p \in ℙ) \to (a \gcd p = 1 \leftrightarrow a \neq p)$
82	56 63 81	syl2anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to (a \gcd p = 1 \leftrightarrow a \neq p)$
83	80 82	mpbird	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a \gcd p = 1$
84		prmz	$⊢ a \in ℙ \to a \in ℤ$
85	56 84	syl	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a \in ℤ$
86		prmz	$⊢ p \in ℙ \to p \in ℤ$
87	63 86	syl	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p \in ℤ$
88	56 57	pccld	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a pCnt \|B\| \in ℕ_{0}$
89		rpexp12i	$⊢ (a \in ℤ \land p \in ℤ \land (a pCnt \|B\| \in ℕ_{0} \land p pCnt \|B\| \in ℕ_{0})) \to (a \gcd p = 1 \to a^{a pCnt \|B\|} \gcd p^{p pCnt \|B\|} = 1)$
90	85 87 88 74 89	syl112anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to (a \gcd p = 1 \to a^{a pCnt \|B\|} \gcd p^{p pCnt \|B\|} = 1)$
91	83 90	mpd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} \gcd p^{p pCnt \|B\|} = 1$
92		coprmdvds2	$⊢ ((a^{a pCnt \|B\|} \in ℤ \land p^{p pCnt \|B\|} \in ℤ \land \|B\| \in ℤ) \land a^{a pCnt \|B\|} \gcd p^{p pCnt \|B\|} = 1) \to ((a^{a pCnt \|B\|} ∥ \|B\| \land p^{p pCnt \|B\|} ∥ \|B\|) \to a^{a pCnt \|B\|} p^{p pCnt \|B\|} ∥ \|B\|)$
93	72 76 77 91 92	syl31anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to ((a^{a pCnt \|B\|} ∥ \|B\| \land p^{p pCnt \|B\|} ∥ \|B\|) \to a^{a pCnt \|B\|} p^{p pCnt \|B\|} ∥ \|B\|)$
94	59 65 93	mp2and	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} p^{p pCnt \|B\|} ∥ \|B\|$
95	68	simp3d	$⊢ (φ \land a \in A) \to \|B\| = a^{a pCnt \|B\|} (\frac{\|B\|}{a^{a pCnt \|B\|}})$
96	95	ad2antrr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to \|B\| = a^{a pCnt \|B\|} (\frac{\|B\|}{a^{a pCnt \|B\|}})$
97	94 96	breqtrd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} p^{p pCnt \|B\|} ∥ a^{a pCnt \|B\|} (\frac{\|B\|}{a^{a pCnt \|B\|}})$
98	69	simprd	$⊢ (φ \land a \in A) \to \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℕ$
99	98	ad2antrr	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℕ$
100	99	nnzd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℤ$
101	71	nnne0d	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to a^{a pCnt \|B\|} \neq 0$
102		dvdscmulr	$⊢ (p^{p pCnt \|B\|} \in ℤ \land \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℤ \land (a^{a pCnt \|B\|} \in ℤ \land a^{a pCnt \|B\|} \neq 0)) \to (a^{a pCnt \|B\|} p^{p pCnt \|B\|} ∥ a^{a pCnt \|B\|} (\frac{\|B\|}{a^{a pCnt \|B\|}}) \leftrightarrow p^{p pCnt \|B\|} ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}}))$
103	76 100 72 101 102	syl112anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to (a^{a pCnt \|B\|} p^{p pCnt \|B\|} ∥ a^{a pCnt \|B\|} (\frac{\|B\|}{a^{a pCnt \|B\|}}) \leftrightarrow p^{p pCnt \|B\|} ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}}))$
104	97 103	mpbid	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to p^{p pCnt \|B\|} ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})$
105	1 2	odcl	$⊢ x \in B \to O (x) \in ℕ_{0}$
106	105	adantl	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to O (x) \in ℕ_{0}$
107	106	nn0zd	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to O (x) \in ℤ$
108		dvdstr	$⊢ (O (x) \in ℤ \land p^{p pCnt \|B\|} \in ℤ \land \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℤ) \to ((O (x) ∥ p^{p pCnt \|B\|} \land p^{p pCnt \|B\|} ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})) \to O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}}))$
109	107 76 100 108	syl3anc	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to ((O (x) ∥ p^{p pCnt \|B\|} \land p^{p pCnt \|B\|} ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})) \to O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}}))$
110	104 109	mpan2d	$⊢ (((φ \land a \in A) \land p \in (A ∖ \{a\})) \land x \in B) \to (O (x) ∥ p^{p pCnt \|B\|} \to O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}}))$
111	110	ss2rabdv	$⊢ ((φ \land a \in A) \land p \in (A ∖ \{a\})) \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
112	44	elpw	$⊢ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in 𝒫 \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} \leftrightarrow \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
113	111 112	sylibr	$⊢ ((φ \land a \in A) \land p \in (A ∖ \{a\})) \to \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\} \in 𝒫 \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
114	3	reseq1i	$⊢ {S ↾}_{(A ∖ \{a\})} = {(p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\}) ↾}_{(A ∖ \{a\})}$
115		difss	$⊢ A ∖ \{a\} \subseteq A$
116		resmpt	$⊢ A ∖ \{a\} \subseteq A \to {(p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\}) ↾}_{(A ∖ \{a\})} = (p \in (A ∖ \{a\}) ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
117	115 116	ax-mp	$⊢ {(p \in A ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\}) ↾}_{(A ∖ \{a\})} = (p \in (A ∖ \{a\}) ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
118	114 117	eqtri	$⊢ {S ↾}_{(A ∖ \{a\})} = (p \in (A ∖ \{a\}) ⟼ \{x \in B \| O (x) ∥ p^{p pCnt \|B\|}\})$
119	113 118	fmptd	$⊢ (φ \land a \in A) \to ({S ↾}_{(A ∖ \{a\})}) : A ∖ \{a\} ⟶ 𝒫 \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
120	119	frnd	$⊢ (φ \land a \in A) \to ran ({S ↾}_{(A ∖ \{a\})}) \subseteq 𝒫 \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
121	54 120	eqsstrid	$⊢ (φ \land a \in A) \to S [A ∖ \{a\}] \subseteq 𝒫 \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
122		sspwuni	$⊢ S [A ∖ \{a\}] \subseteq 𝒫 \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} \leftrightarrow ⋃ S [A ∖ \{a\}] \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
123	121 122	sylib	$⊢ (φ \land a \in A) \to ⋃ S [A ∖ \{a\}] \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
124	98	nnzd	$⊢ (φ \land a \in A) \to \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℤ$
125	2 1	oddvdssubg	$⊢ (G \in Abel \land \frac{\|B\|}{a^{a pCnt \|B\|}} \in ℤ) \to \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} \in SubGrp (G)$
126	49 124 125	syl2anc	$⊢ (φ \land a \in A) \to \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} \in SubGrp (G)$
127	9	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ S [A ∖ \{a\}] \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} \land \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} \in SubGrp (G)) \to mrCls (SubGrp (G)) (⋃ S [A ∖ \{a\}]) \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
128	53 123 126 127	syl3anc	$⊢ (φ \land a \in A) \to mrCls (SubGrp (G)) (⋃ S [A ∖ \{a\}]) \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
129		ss2in	$⊢ (S (a) \subseteq \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} \land mrCls (SubGrp (G)) (⋃ S [A ∖ \{a\}]) \subseteq \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}) \to S (a) \cap mrCls (SubGrp (G)) (⋃ S [A ∖ \{a\}]) \subseteq \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} \cap \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
130	48 128 129	syl2anc	$⊢ (φ \land a \in A) \to S (a) \cap mrCls (SubGrp (G)) (⋃ S [A ∖ \{a\}]) \subseteq \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} \cap \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
131		eqid	$⊢ \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} = \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\}$
132		eqid	$⊢ \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} = \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\}$
133	68	simp2d	$⊢ (φ \land a \in A) \to a^{a pCnt \|B\|} \gcd (\frac{\|B\|}{a^{a pCnt \|B\|}}) = 1$
134		eqid	$⊢ LSSum (G) = LSSum (G)$
135	1 2 131 132 49 70 98 133 95 8 134	ablfacrp	$⊢ (φ \land a \in A) \to (\{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} \cap \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} = \{0_{G}\} \land \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} LSSum (G) \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} = B)$
136	135	simpld	$⊢ (φ \land a \in A) \to \{x \in B \| O (x) ∥ a^{a pCnt \|B\|}\} \cap \{x \in B \| O (x) ∥ (\frac{\|B\|}{a^{a pCnt \|B\|}})\} = \{0_{G}\}$
137	130 136	sseqtrd	$⊢ (φ \land a \in A) \to S (a) \cap mrCls (SubGrp (G)) (⋃ S [A ∖ \{a\}]) \subseteq \{0_{G}\}$
138	7 8 9 11 14 30 37 137	dmdprdd	$⊢ φ \to G dom DProd S$

Metamath Proof Explorer

Theorem ablfac1b

Proof