pgpfac1lem3a

	Ref	Expression
Hypotheses	pgpfac1.k	$⊢ K = mrCls (SubGrp (G))$
	pgpfac1.s	$⊢ S = K (\{A\})$
	pgpfac1.b	$⊢ B = {Base}_{G}$
	pgpfac1.o	$⊢ O = od (G)$
	pgpfac1.e	$⊢ E = gEx (G)$
	pgpfac1.z	$⊢ \underset{˙}{0} = 0_{G}$
	pgpfac1.l	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	pgpfac1.p	$⊢ φ \to P pGrp G$
	pgpfac1.g	$⊢ φ \to G \in Abel$
	pgpfac1.n	$⊢ φ \to B \in Fin$
	pgpfac1.oe	$⊢ φ \to O (A) = E$
	pgpfac1.u	$⊢ φ \to U \in SubGrp (G)$
	pgpfac1.au	$⊢ φ \to A \in U$
	pgpfac1.w	$⊢ φ \to W \in SubGrp (G)$
	pgpfac1.i	$⊢ φ \to S \cap W = \{\underset{˙}{0}\}$
	pgpfac1.ss	$⊢ φ \to S \underset{˙}{\oplus} W \subseteq U$
	pgpfac1.2	$⊢ φ \to \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg S \underset{˙}{\oplus} W \subset w)$
	pgpfac1.c	$⊢ φ \to C \in (U ∖ (S \underset{˙}{\oplus} W))$
	pgpfac1.mg	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	pgpfac1.m	$⊢ φ \to M \in ℤ$
	pgpfac1.mw	$⊢ φ \to (P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A) \in W$
Assertion	pgpfac1lem3a	$⊢ φ \to (P ∥ E \land P ∥ M)$

Proof

Step	Hyp	Ref	Expression
1		pgpfac1.k	$⊢ K = mrCls (SubGrp (G))$
2		pgpfac1.s	$⊢ S = K (\{A\})$
3		pgpfac1.b	$⊢ B = {Base}_{G}$
4		pgpfac1.o	$⊢ O = od (G)$
5		pgpfac1.e	$⊢ E = gEx (G)$
6		pgpfac1.z	$⊢ \underset{˙}{0} = 0_{G}$
7		pgpfac1.l	$⊢ \underset{˙}{\oplus} = LSSum (G)$
8		pgpfac1.p	$⊢ φ \to P pGrp G$
9		pgpfac1.g	$⊢ φ \to G \in Abel$
10		pgpfac1.n	$⊢ φ \to B \in Fin$
11		pgpfac1.oe	$⊢ φ \to O (A) = E$
12		pgpfac1.u	$⊢ φ \to U \in SubGrp (G)$
13		pgpfac1.au	$⊢ φ \to A \in U$
14		pgpfac1.w	$⊢ φ \to W \in SubGrp (G)$
15		pgpfac1.i	$⊢ φ \to S \cap W = \{\underset{˙}{0}\}$
16		pgpfac1.ss	$⊢ φ \to S \underset{˙}{\oplus} W \subseteq U$
17		pgpfac1.2	$⊢ φ \to \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg S \underset{˙}{\oplus} W \subset w)$
18		pgpfac1.c	$⊢ φ \to C \in (U ∖ (S \underset{˙}{\oplus} W))$
19		pgpfac1.mg	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
20		pgpfac1.m	$⊢ φ \to M \in ℤ$
21		pgpfac1.mw	$⊢ φ \to (P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A) \in W$
22	18	eldifbd	$⊢ φ \to \neg C \in (S \underset{˙}{\oplus} W)$
23		pgpprm	$⊢ P pGrp G \to P \in ℙ$
24	8 23	syl	$⊢ φ \to P \in ℙ$
25		ablgrp	$⊢ G \in Abel \to G \in Grp$
26	9 25	syl	$⊢ φ \to G \in Grp$
27	3 5	gexcl2	$⊢ (G \in Grp \land B \in Fin) \to E \in ℕ$
28	26 10 27	syl2anc	$⊢ φ \to E \in ℕ$
29		pceq0	$⊢ (P \in ℙ \land E \in ℕ) \to (P pCnt E = 0 \leftrightarrow \neg P ∥ E)$
30	24 28 29	syl2anc	$⊢ φ \to (P pCnt E = 0 \leftrightarrow \neg P ∥ E)$
31		oveq2	$⊢ P pCnt E = 0 \to P^{P pCnt E} = P^{0}$
32	30 31	biimtrrdi	$⊢ φ \to (\neg P ∥ E \to P^{P pCnt E} = P^{0})$
33	3	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
34	26 33	syl	$⊢ φ \to B \neq \emptyset$
35		hashnncl	$⊢ B \in Fin \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
36	10 35	syl	$⊢ φ \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
37	34 36	mpbird	$⊢ φ \to \|B\| \in ℕ$
38	24 37	pccld	$⊢ φ \to P pCnt \|B\| \in ℕ_{0}$
39	3 5	gexdvds3	$⊢ (G \in Grp \land B \in Fin) \to E ∥ \|B\|$
40	26 10 39	syl2anc	$⊢ φ \to E ∥ \|B\|$
41	3	pgphash	$⊢ (P pGrp G \land B \in Fin) \to \|B\| = P^{P pCnt \|B\|}$
42	8 10 41	syl2anc	$⊢ φ \to \|B\| = P^{P pCnt \|B\|}$
43	40 42	breqtrd	$⊢ φ \to E ∥ P^{P pCnt \|B\|}$
44		oveq2	$⊢ k = P pCnt \|B\| \to P^{k} = P^{P pCnt \|B\|}$
45	44	breq2d	$⊢ k = P pCnt \|B\| \to (E ∥ P^{k} \leftrightarrow E ∥ P^{P pCnt \|B\|})$
46	45	rspcev	$⊢ (P pCnt \|B\| \in ℕ_{0} \land E ∥ P^{P pCnt \|B\|}) \to \exists k \in ℕ_{0} E ∥ P^{k}$
47	38 43 46	syl2anc	$⊢ φ \to \exists k \in ℕ_{0} E ∥ P^{k}$
48		pcprmpw2	$⊢ (P \in ℙ \land E \in ℕ) \to (\exists k \in ℕ_{0} E ∥ P^{k} \leftrightarrow E = P^{P pCnt E})$
49	24 28 48	syl2anc	$⊢ φ \to (\exists k \in ℕ_{0} E ∥ P^{k} \leftrightarrow E = P^{P pCnt E})$
50	47 49	mpbid	$⊢ φ \to E = P^{P pCnt E}$
51	50	eqcomd	$⊢ φ \to P^{P pCnt E} = E$
52		prmnn	$⊢ P \in ℙ \to P \in ℕ$
53	24 52	syl	$⊢ φ \to P \in ℕ$
54	53	nncnd	$⊢ φ \to P \in ℂ$
55	54	exp0d	$⊢ φ \to P^{0} = 1$
56	51 55	eqeq12d	$⊢ φ \to (P^{P pCnt E} = P^{0} \leftrightarrow E = 1)$
57	26	grpmndd	$⊢ φ \to G \in Mnd$
58	3 5	gex1	$⊢ G \in Mnd \to (E = 1 \leftrightarrow B \approx 1_{𝑜})$
59	57 58	syl	$⊢ φ \to (E = 1 \leftrightarrow B \approx 1_{𝑜})$
60	56 59	bitrd	$⊢ φ \to (P^{P pCnt E} = P^{0} \leftrightarrow B \approx 1_{𝑜})$
61	32 60	sylibd	$⊢ φ \to (\neg P ∥ E \to B \approx 1_{𝑜})$
62	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (B)$
63	26 62	syl	$⊢ φ \to SubGrp (G) \in ACS (B)$
64	63	acsmred	$⊢ φ \to SubGrp (G) \in Moore (B)$
65	3	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
66	12 65	syl	$⊢ φ \to U \subseteq B$
67	66 13	sseldd	$⊢ φ \to A \in B$
68	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land A \in B) \to K (\{A\}) \in SubGrp (G)$
69	64 67 68	syl2anc	$⊢ φ \to K (\{A\}) \in SubGrp (G)$
70	2 69	eqeltrid	$⊢ φ \to S \in SubGrp (G)$
71	7	lsmsubg2	$⊢ (G \in Abel \land S \in SubGrp (G) \land W \in SubGrp (G)) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
72	9 70 14 71	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} W \in SubGrp (G)$
73	6	subg0cl	$⊢ S \underset{˙}{\oplus} W \in SubGrp (G) \to \underset{˙}{0} \in (S \underset{˙}{\oplus} W)$
74	72 73	syl	$⊢ φ \to \underset{˙}{0} \in (S \underset{˙}{\oplus} W)$
75	74	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq S \underset{˙}{\oplus} W$
76	75	adantr	$⊢ (φ \land B \approx 1_{𝑜}) \to \{\underset{˙}{0}\} \subseteq S \underset{˙}{\oplus} W$
77	18	eldifad	$⊢ φ \to C \in U$
78	66 77	sseldd	$⊢ φ \to C \in B$
79	78	adantr	$⊢ (φ \land B \approx 1_{𝑜}) \to C \in B$
80	3 6	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
81	26 80	syl	$⊢ φ \to \underset{˙}{0} \in B$
82		en1eqsn	$⊢ (\underset{˙}{0} \in B \land B \approx 1_{𝑜}) \to B = \{\underset{˙}{0}\}$
83	81 82	sylan	$⊢ (φ \land B \approx 1_{𝑜}) \to B = \{\underset{˙}{0}\}$
84	79 83	eleqtrd	$⊢ (φ \land B \approx 1_{𝑜}) \to C \in \{\underset{˙}{0}\}$
85	76 84	sseldd	$⊢ (φ \land B \approx 1_{𝑜}) \to C \in (S \underset{˙}{\oplus} W)$
86	85	ex	$⊢ φ \to (B \approx 1_{𝑜} \to C \in (S \underset{˙}{\oplus} W))$
87	61 86	syld	$⊢ φ \to (\neg P ∥ E \to C \in (S \underset{˙}{\oplus} W))$
88	22 87	mt3d	$⊢ φ \to P ∥ E$
89	28	nncnd	$⊢ φ \to E \in ℂ$
90	53	nnne0d	$⊢ φ \to P \neq 0$
91	89 54 90	divcan1d	$⊢ φ \to (\frac{E}{P}) P = E$
92	11 91	eqtr4d	$⊢ φ \to O (A) = (\frac{E}{P}) P$
93		nndivdvds	$⊢ (E \in ℕ \land P \in ℕ) \to (P ∥ E \leftrightarrow \frac{E}{P} \in ℕ)$
94	28 53 93	syl2anc	$⊢ φ \to (P ∥ E \leftrightarrow \frac{E}{P} \in ℕ)$
95	88 94	mpbid	$⊢ φ \to \frac{E}{P} \in ℕ$
96	95	nnzd	$⊢ φ \to \frac{E}{P} \in ℤ$
97	96 20	zmulcld	$⊢ φ \to (\frac{E}{P}) \cdot M \in ℤ$
98	67	snssd	$⊢ φ \to \{A\} \subseteq B$
99	64 1 98	mrcssidd	$⊢ φ \to \{A\} \subseteq K (\{A\})$
100	99 2	sseqtrrdi	$⊢ φ \to \{A\} \subseteq S$
101		snssg	$⊢ A \in U \to (A \in S \leftrightarrow \{A\} \subseteq S)$
102	13 101	syl	$⊢ φ \to (A \in S \leftrightarrow \{A\} \subseteq S)$
103	100 102	mpbird	$⊢ φ \to A \in S$
104	19	subgmulgcl	$⊢ (S \in SubGrp (G) \land (\frac{E}{P}) \cdot M \in ℤ \land A \in S) \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in S$
105	70 97 103 104	syl3anc	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in S$
106		prmz	$⊢ P \in ℙ \to P \in ℤ$
107	24 106	syl	$⊢ φ \to P \in ℤ$
108	3 19	mulgcl	$⊢ (G \in Grp \land P \in ℤ \land C \in B) \to P \underset{˙}{\cdot} C \in B$
109	26 107 78 108	syl3anc	$⊢ φ \to P \underset{˙}{\cdot} C \in B$
110	3 19	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land A \in B) \to M \underset{˙}{\cdot} A \in B$
111	26 20 67 110	syl3anc	$⊢ φ \to M \underset{˙}{\cdot} A \in B$
112		eqid	$⊢ +_{G} = +_{G}$
113	3 19 112	mulgdi	$⊢ (G \in Abel \land (\frac{E}{P} \in ℤ \land P \underset{˙}{\cdot} C \in B \land M \underset{˙}{\cdot} A \in B)) \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) = ((\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) +_{G} ((\frac{E}{P}) \underset{˙}{\cdot} (M \underset{˙}{\cdot} A))$
114	9 96 109 111 113	syl13anc	$⊢ φ \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) = ((\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) +_{G} ((\frac{E}{P}) \underset{˙}{\cdot} (M \underset{˙}{\cdot} A))$
115	91	oveq1d	$⊢ φ \to (\frac{E}{P}) P \underset{˙}{\cdot} C = E \underset{˙}{\cdot} C$
116	3 19	mulgass	$⊢ (G \in Grp \land (\frac{E}{P} \in ℤ \land P \in ℤ \land C \in B)) \to (\frac{E}{P}) P \underset{˙}{\cdot} C = (\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
117	26 96 107 78 116	syl13anc	$⊢ φ \to (\frac{E}{P}) P \underset{˙}{\cdot} C = (\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
118	3 5 19 6	gexid	$⊢ C \in B \to E \underset{˙}{\cdot} C = \underset{˙}{0}$
119	78 118	syl	$⊢ φ \to E \underset{˙}{\cdot} C = \underset{˙}{0}$
120	115 117 119	3eqtr3rd	$⊢ φ \to \underset{˙}{0} = (\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
121	3 19	mulgass	$⊢ (G \in Grp \land (\frac{E}{P} \in ℤ \land M \in ℤ \land A \in B)) \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = (\frac{E}{P}) \underset{˙}{\cdot} (M \underset{˙}{\cdot} A)$
122	26 96 20 67 121	syl13anc	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = (\frac{E}{P}) \underset{˙}{\cdot} (M \underset{˙}{\cdot} A)$
123	120 122	oveq12d	$⊢ φ \to \underset{˙}{0} +_{G} ((\frac{E}{P}) \cdot M \underset{˙}{\cdot} A) = ((\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) +_{G} ((\frac{E}{P}) \underset{˙}{\cdot} (M \underset{˙}{\cdot} A))$
124	3	subgss	$⊢ S \in SubGrp (G) \to S \subseteq B$
125	70 124	syl	$⊢ φ \to S \subseteq B$
126	125 105	sseldd	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in B$
127	3 112 6	grplid	$⊢ (G \in Grp \land (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in B) \to \underset{˙}{0} +_{G} ((\frac{E}{P}) \cdot M \underset{˙}{\cdot} A) = (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A$
128	26 126 127	syl2anc	$⊢ φ \to \underset{˙}{0} +_{G} ((\frac{E}{P}) \cdot M \underset{˙}{\cdot} A) = (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A$
129	114 123 128	3eqtr2d	$⊢ φ \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) = (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A$
130	19	subgmulgcl	$⊢ (W \in SubGrp (G) \land \frac{E}{P} \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A) \in W) \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) \in W$
131	14 96 21 130	syl3anc	$⊢ φ \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) \in W$
132	129 131	eqeltrrd	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in W$
133	105 132	elind	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in (S \cap W)$
134	133 15	eleqtrd	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in \{\underset{˙}{0}\}$
135		elsni	$⊢ (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in \{\underset{˙}{0}\} \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0}$
136	134 135	syl	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0}$
137	3 4 19 6	oddvds	$⊢ (G \in Grp \land A \in B \land (\frac{E}{P}) \cdot M \in ℤ) \to (O (A) ∥ (\frac{E}{P}) \cdot M \leftrightarrow (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0})$
138	26 67 97 137	syl3anc	$⊢ φ \to (O (A) ∥ (\frac{E}{P}) \cdot M \leftrightarrow (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0})$
139	136 138	mpbird	$⊢ φ \to O (A) ∥ (\frac{E}{P}) \cdot M$
140	92 139	eqbrtrrd	$⊢ φ \to (\frac{E}{P}) P ∥ (\frac{E}{P}) \cdot M$
141	95	nnne0d	$⊢ φ \to \frac{E}{P} \neq 0$
142		dvdscmulr	$⊢ (P \in ℤ \land M \in ℤ \land (\frac{E}{P} \in ℤ \land \frac{E}{P} \neq 0)) \to ((\frac{E}{P}) P ∥ (\frac{E}{P}) \cdot M \leftrightarrow P ∥ M)$
143	107 20 96 141 142	syl112anc	$⊢ φ \to ((\frac{E}{P}) P ∥ (\frac{E}{P}) \cdot M \leftrightarrow P ∥ M)$
144	140 143	mpbid	$⊢ φ \to P ∥ M$
145	88 144	jca	$⊢ φ \to (P ∥ E \land P ∥ M)$

Metamath Proof Explorer

Theorem pgpfac1lem3a

Proof