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	syl6bir	$⊢ φ \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		grpmnd	$⊢ G \in Grp \to G \in Mnd$
58	26 57	syl	$⊢ φ \to G \in Mnd$
59	3 5	gex1	$⊢ G \in Mnd \to (E = 1 \leftrightarrow B \approx 1_{𝑜})$
60	58 59	syl	$⊢ φ \to (E = 1 \leftrightarrow B \approx 1_{𝑜})$
61	56 60	bitrd	$⊢ φ \to (P^{P pCnt E} = P^{0} \leftrightarrow B \approx 1_{𝑜})$
62	32 61	sylibd	$⊢ φ \to (\neg P ∥ E \to B \approx 1_{𝑜})$
63	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (B)$
64	26 63	syl	$⊢ φ \to SubGrp (G) \in ACS (B)$
65	64	acsmred	$⊢ φ \to SubGrp (G) \in Moore (B)$
66	3	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
67	12 66	syl	$⊢ φ \to U \subseteq B$
68	67 13	sseldd	$⊢ φ \to A \in B$
69	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land A \in B) \to K (\{A\}) \in SubGrp (G)$
70	65 68 69	syl2anc	$⊢ φ \to K (\{A\}) \in SubGrp (G)$
71	2 70	eqeltrid	$⊢ φ \to S \in SubGrp (G)$
72	7	lsmsubg2	$⊢ (G \in Abel \land S \in SubGrp (G) \land W \in SubGrp (G)) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
73	9 71 14 72	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} W \in SubGrp (G)$
74	6	subg0cl	$⊢ S \underset{˙}{\oplus} W \in SubGrp (G) \to \underset{˙}{0} \in (S \underset{˙}{\oplus} W)$
75	73 74	syl	$⊢ φ \to \underset{˙}{0} \in (S \underset{˙}{\oplus} W)$
76	75	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq S \underset{˙}{\oplus} W$
77	76	adantr	$⊢ (φ \land B \approx 1_{𝑜}) \to \{\underset{˙}{0}\} \subseteq S \underset{˙}{\oplus} W$
78	18	eldifad	$⊢ φ \to C \in U$
79	67 78	sseldd	$⊢ φ \to C \in B$
80	79	adantr	$⊢ (φ \land B \approx 1_{𝑜}) \to C \in B$
81	3 6	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
82	26 81	syl	$⊢ φ \to \underset{˙}{0} \in B$
83		en1eqsn	$⊢ (\underset{˙}{0} \in B \land B \approx 1_{𝑜}) \to B = \{\underset{˙}{0}\}$
84	82 83	sylan	$⊢ (φ \land B \approx 1_{𝑜}) \to B = \{\underset{˙}{0}\}$
85	80 84	eleqtrd	$⊢ (φ \land B \approx 1_{𝑜}) \to C \in \{\underset{˙}{0}\}$
86	77 85	sseldd	$⊢ (φ \land B \approx 1_{𝑜}) \to C \in (S \underset{˙}{\oplus} W)$
87	86	ex	$⊢ φ \to (B \approx 1_{𝑜} \to C \in (S \underset{˙}{\oplus} W))$
88	62 87	syld	$⊢ φ \to (\neg P ∥ E \to C \in (S \underset{˙}{\oplus} W))$
89	22 88	mt3d	$⊢ φ \to P ∥ E$
90	28	nncnd	$⊢ φ \to E \in ℂ$
91	53	nnne0d	$⊢ φ \to P \neq 0$
92	90 54 91	divcan1d	$⊢ φ \to (\frac{E}{P}) P = E$
93	11 92	eqtr4d	$⊢ φ \to O (A) = (\frac{E}{P}) P$
94		nndivdvds	$⊢ (E \in ℕ \land P \in ℕ) \to (P ∥ E \leftrightarrow \frac{E}{P} \in ℕ)$
95	28 53 94	syl2anc	$⊢ φ \to (P ∥ E \leftrightarrow \frac{E}{P} \in ℕ)$
96	89 95	mpbid	$⊢ φ \to \frac{E}{P} \in ℕ$
97	96	nnzd	$⊢ φ \to \frac{E}{P} \in ℤ$
98	97 20	zmulcld	$⊢ φ \to (\frac{E}{P}) \cdot M \in ℤ$
99	68	snssd	$⊢ φ \to \{A\} \subseteq B$
100	65 1 99	mrcssidd	$⊢ φ \to \{A\} \subseteq K (\{A\})$
101	100 2	sseqtrrdi	$⊢ φ \to \{A\} \subseteq S$
102		snssg	$⊢ A \in U \to (A \in S \leftrightarrow \{A\} \subseteq S)$
103	13 102	syl	$⊢ φ \to (A \in S \leftrightarrow \{A\} \subseteq S)$
104	101 103	mpbird	$⊢ φ \to A \in S$
105	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$
106	71 98 104 105	syl3anc	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in S$
107		prmz	$⊢ P \in ℙ \to P \in ℤ$
108	24 107	syl	$⊢ φ \to P \in ℤ$
109	3 19	mulgcl	$⊢ (G \in Grp \land P \in ℤ \land C \in B) \to P \underset{˙}{\cdot} C \in B$
110	26 108 79 109	syl3anc	$⊢ φ \to P \underset{˙}{\cdot} C \in B$
111	3 19	mulgcl	$⊢ (G \in Grp \land M \in ℤ \land A \in B) \to M \underset{˙}{\cdot} A \in B$
112	26 20 68 111	syl3anc	$⊢ φ \to M \underset{˙}{\cdot} A \in B$
113		eqid	$⊢ +_{G} = +_{G}$
114	3 19 113	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))$
115	9 97 110 112 114	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))$
116	92	oveq1d	$⊢ φ \to (\frac{E}{P}) P \underset{˙}{\cdot} C = E \underset{˙}{\cdot} C$
117	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)$
118	26 97 108 79 117	syl13anc	$⊢ φ \to (\frac{E}{P}) P \underset{˙}{\cdot} C = (\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
119	3 5 19 6	gexid	$⊢ C \in B \to E \underset{˙}{\cdot} C = \underset{˙}{0}$
120	79 119	syl	$⊢ φ \to E \underset{˙}{\cdot} C = \underset{˙}{0}$
121	116 118 120	3eqtr3rd	$⊢ φ \to \underset{˙}{0} = (\frac{E}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
122	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)$
123	26 97 20 68 122	syl13anc	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = (\frac{E}{P}) \underset{˙}{\cdot} (M \underset{˙}{\cdot} A)$
124	121 123	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))$
125	3	subgss	$⊢ S \in SubGrp (G) \to S \subseteq B$
126	71 125	syl	$⊢ φ \to S \subseteq B$
127	126 106	sseldd	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in B$
128	3 113 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$
129	26 127 128	syl2anc	$⊢ φ \to \underset{˙}{0} +_{G} ((\frac{E}{P}) \cdot M \underset{˙}{\cdot} A) = (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A$
130	115 124 129	3eqtr2d	$⊢ φ \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) = (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A$
131	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$
132	14 97 21 131	syl3anc	$⊢ φ \to (\frac{E}{P}) \underset{˙}{\cdot} ((P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)) \in W$
133	130 132	eqeltrrd	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in W$
134	106 133	elind	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in (S \cap W)$
135	134 15	eleqtrd	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in \{\underset{˙}{0}\}$
136		elsni	$⊢ (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A \in \{\underset{˙}{0}\} \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0}$
137	135 136	syl	$⊢ φ \to (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0}$
138	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})$
139	26 68 98 138	syl3anc	$⊢ φ \to (O (A) ∥ (\frac{E}{P}) \cdot M \leftrightarrow (\frac{E}{P}) \cdot M \underset{˙}{\cdot} A = \underset{˙}{0})$
140	137 139	mpbird	$⊢ φ \to O (A) ∥ (\frac{E}{P}) \cdot M$
141	93 140	eqbrtrrd	$⊢ φ \to (\frac{E}{P}) P ∥ (\frac{E}{P}) \cdot M$
142	96	nnne0d	$⊢ φ \to \frac{E}{P} \neq 0$
143		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)$
144	108 20 97 142 143	syl112anc	$⊢ φ \to ((\frac{E}{P}) P ∥ (\frac{E}{P}) \cdot M \leftrightarrow P ∥ M)$
145	141 144	mpbid	$⊢ φ \to P ∥ M$
146	89 145	jca	$⊢ φ \to (P ∥ E \land P ∥ M)$

Metamath Proof Explorer

Theorem pgpfac1lem3a

Proof