pgpfac1lem2

	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}$
Assertion	pgpfac1lem2	$⊢ φ \to P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)$

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	18	eldifbd	$⊢ φ \to \neg C \in (S \underset{˙}{\oplus} W)$
21	18	eldifad	$⊢ φ \to C \in U$
22	21	adantr	$⊢ (φ \land \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to C \in U$
23		pgpprm	$⊢ P pGrp G \to P \in ℙ$
24	8 23	syl	$⊢ φ \to P \in ℙ$
25		prmz	$⊢ P \in ℙ \to P \in ℤ$
26	24 25	syl	$⊢ φ \to P \in ℤ$
27	19	subgmulgcl	$⊢ (U \in SubGrp (G) \land P \in ℤ \land C \in U) \to P \underset{˙}{\cdot} C \in U$
28	12 26 21 27	syl3anc	$⊢ φ \to P \underset{˙}{\cdot} C \in U$
29	28	adantr	$⊢ (φ \land \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to P \underset{˙}{\cdot} C \in U$
30		simpr	$⊢ (φ \land \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)$
31	29 30	eldifd	$⊢ (φ \land \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to P \underset{˙}{\cdot} C \in (U ∖ (S \underset{˙}{\oplus} W))$
32	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pgpfac1lem1	$⊢ (φ \land P \underset{˙}{\cdot} C \in (U ∖ (S \underset{˙}{\oplus} W))) \to (S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{P \underset{˙}{\cdot} C\}) = U$
33	31 32	syldan	$⊢ (φ \land \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to (S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{P \underset{˙}{\cdot} C\}) = U$
34	22 33	eleqtrrd	$⊢ (φ \land \neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to C \in ((S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{P \underset{˙}{\cdot} C\}))$
35	34	ex	$⊢ φ \to (\neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in ((S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{P \underset{˙}{\cdot} C\})))$
36		eqid	$⊢ -_{G} = -_{G}$
37		ablgrp	$⊢ G \in Abel \to G \in Grp$
38	9 37	syl	$⊢ φ \to G \in Grp$
39	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (B)$
40	38 39	syl	$⊢ φ \to SubGrp (G) \in ACS (B)$
41	40	acsmred	$⊢ φ \to SubGrp (G) \in Moore (B)$
42	3	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
43	12 42	syl	$⊢ φ \to U \subseteq B$
44	43 13	sseldd	$⊢ φ \to A \in B$
45	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land A \in B) \to K (\{A\}) \in SubGrp (G)$
46	41 44 45	syl2anc	$⊢ φ \to K (\{A\}) \in SubGrp (G)$
47	2 46	eqeltrid	$⊢ φ \to S \in SubGrp (G)$
48	7	lsmsubg2	$⊢ (G \in Abel \land S \in SubGrp (G) \land W \in SubGrp (G)) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
49	9 47 14 48	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} W \in SubGrp (G)$
50	43 28	sseldd	$⊢ φ \to P \underset{˙}{\cdot} C \in B$
51	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land P \underset{˙}{\cdot} C \in B) \to K (\{P \underset{˙}{\cdot} C\}) \in SubGrp (G)$
52	41 50 51	syl2anc	$⊢ φ \to K (\{P \underset{˙}{\cdot} C\}) \in SubGrp (G)$
53	36 7 49 52	lsmelvalm	$⊢ φ \to (C \in ((S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{P \underset{˙}{\cdot} C\})) \leftrightarrow \exists s \in (S \underset{˙}{\oplus} W) \exists t \in K (\{P \underset{˙}{\cdot} C\}) C = s -_{G} t)$
54		eqid	$⊢ (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
55	3 19 54 1	cycsubg2	$⊢ (G \in Grp \land P \underset{˙}{\cdot} C \in B) \to K (\{P \underset{˙}{\cdot} C\}) = ran (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
56	38 50 55	syl2anc	$⊢ φ \to K (\{P \underset{˙}{\cdot} C\}) = ran (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
57	56	rexeqdv	$⊢ φ \to (\exists t \in K (\{P \underset{˙}{\cdot} C\}) C = s -_{G} t \leftrightarrow \exists t \in ran (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) C = s -_{G} t)$
58		ovex	$⊢ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \in V$
59	58	rgenw	$⊢ \forall k \in ℤ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \in V$
60		oveq2	$⊢ t = k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \to s -_{G} t = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
61	60	eqeq2d	$⊢ t = k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \to (C = s -_{G} t \leftrightarrow C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)))$
62	54 61	rexrnmptw	$⊢ \forall k \in ℤ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \in V \to (\exists t \in ran (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) C = s -_{G} t \leftrightarrow \exists k \in ℤ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)))$
63	59 62	mp1i	$⊢ φ \to (\exists t \in ran (k \in ℤ ⟼ k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) C = s -_{G} t \leftrightarrow \exists k \in ℤ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)))$
64	57 63	bitrd	$⊢ φ \to (\exists t \in K (\{P \underset{˙}{\cdot} C\}) C = s -_{G} t \leftrightarrow \exists k \in ℤ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)))$
65	64	rexbidv	$⊢ φ \to (\exists s \in (S \underset{˙}{\oplus} W) \exists t \in K (\{P \underset{˙}{\cdot} C\}) C = s -_{G} t \leftrightarrow \exists s \in (S \underset{˙}{\oplus} W) \exists k \in ℤ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)))$
66		rexcom	$⊢ \exists s \in (S \underset{˙}{\oplus} W) \exists k \in ℤ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow \exists k \in ℤ \exists s \in (S \underset{˙}{\oplus} W) C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
67	38	ad2antrr	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to G \in Grp$
68	16 43	sstrd	$⊢ φ \to S \underset{˙}{\oplus} W \subseteq B$
69	68	adantr	$⊢ (φ \land k \in ℤ) \to S \underset{˙}{\oplus} W \subseteq B$
70	69	sselda	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to s \in B$
71		simplr	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to k \in ℤ$
72	50	ad2antrr	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to P \underset{˙}{\cdot} C \in B$
73	3 19	mulgcl	$⊢ (G \in Grp \land k \in ℤ \land P \underset{˙}{\cdot} C \in B) \to k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \in B$
74	67 71 72 73	syl3anc	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \in B$
75	43 21	sseldd	$⊢ φ \to C \in B$
76	75	ad2antrr	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to C \in B$
77		eqid	$⊢ +_{G} = +_{G}$
78	3 77 36	grpsubadd	$⊢ (G \in Grp \land (s \in B \land k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C) \in B \land C \in B)) \to (s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = C \leftrightarrow C +_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = s)$
79	67 70 74 76 78	syl13anc	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to (s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = C \leftrightarrow C +_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = s)$
80		1zzd	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to 1 \in ℤ$
81	26	ad2antrr	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to P \in ℤ$
82	71 81	zmulcld	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to k P \in ℤ$
83	3 19 77	mulgdir	$⊢ (G \in Grp \land (1 \in ℤ \land k P \in ℤ \land C \in B)) \to (1 + k P) \underset{˙}{\cdot} C = (1 \underset{˙}{\cdot} C) +_{G} (k P \underset{˙}{\cdot} C)$
84	67 80 82 76 83	syl13anc	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to (1 + k P) \underset{˙}{\cdot} C = (1 \underset{˙}{\cdot} C) +_{G} (k P \underset{˙}{\cdot} C)$
85	3 19	mulg1	$⊢ C \in B \to 1 \underset{˙}{\cdot} C = C$
86	76 85	syl	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to 1 \underset{˙}{\cdot} C = C$
87	3 19	mulgass	$⊢ (G \in Grp \land (k \in ℤ \land P \in ℤ \land C \in B)) \to k P \underset{˙}{\cdot} C = k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
88	67 71 81 76 87	syl13anc	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to k P \underset{˙}{\cdot} C = k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)$
89	86 88	oveq12d	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to (1 \underset{˙}{\cdot} C) +_{G} (k P \underset{˙}{\cdot} C) = C +_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
90	84 89	eqtrd	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to (1 + k P) \underset{˙}{\cdot} C = C +_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C))$
91	90	eqeq1d	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to ((1 + k P) \underset{˙}{\cdot} C = s \leftrightarrow C +_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = s)$
92	79 91	bitr4d	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to (s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = C \leftrightarrow (1 + k P) \underset{˙}{\cdot} C = s)$
93		eqcom	$⊢ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) = C$
94		eqcom	$⊢ s = (1 + k P) \underset{˙}{\cdot} C \leftrightarrow (1 + k P) \underset{˙}{\cdot} C = s$
95	92 93 94	3bitr4g	$⊢ ((φ \land k \in ℤ) \land s \in (S \underset{˙}{\oplus} W)) \to (C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow s = (1 + k P) \underset{˙}{\cdot} C)$
96	95	rexbidva	$⊢ (φ \land k \in ℤ) \to (\exists s \in (S \underset{˙}{\oplus} W) C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow \exists s \in (S \underset{˙}{\oplus} W) s = (1 + k P) \underset{˙}{\cdot} C)$
97		risset	$⊢ (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \leftrightarrow \exists s \in (S \underset{˙}{\oplus} W) s = (1 + k P) \underset{˙}{\cdot} C$
98	96 97	bitr4di	$⊢ (φ \land k \in ℤ) \to (\exists s \in (S \underset{˙}{\oplus} W) C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W))$
99	98	rexbidva	$⊢ φ \to (\exists k \in ℤ \exists s \in (S \underset{˙}{\oplus} W) C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow \exists k \in ℤ (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W))$
100	66 99	bitrid	$⊢ φ \to (\exists s \in (S \underset{˙}{\oplus} W) \exists k \in ℤ C = s -_{G} (k \underset{˙}{\cdot} (P \underset{˙}{\cdot} C)) \leftrightarrow \exists k \in ℤ (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W))$
101	53 65 100	3bitrd	$⊢ φ \to (C \in ((S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{P \underset{˙}{\cdot} C\})) \leftrightarrow \exists k \in ℤ (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W))$
102	35 101	sylibd	$⊢ φ \to (\neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to \exists k \in ℤ (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W))$
103	38	adantr	$⊢ (φ \land k \in ℤ) \to G \in Grp$
104	75	adantr	$⊢ (φ \land k \in ℤ) \to C \in B$
105		1z	$⊢ 1 \in ℤ$
106		id	$⊢ k \in ℤ \to k \in ℤ$
107		zmulcl	$⊢ (k \in ℤ \land P \in ℤ) \to k P \in ℤ$
108	106 26 107	syl2anr	$⊢ (φ \land k \in ℤ) \to k P \in ℤ$
109		zaddcl	$⊢ (1 \in ℤ \land k P \in ℤ) \to 1 + k P \in ℤ$
110	105 108 109	sylancr	$⊢ (φ \land k \in ℤ) \to 1 + k P \in ℤ$
111	3 4	odcl	$⊢ C \in B \to O (C) \in ℕ_{0}$
112	104 111	syl	$⊢ (φ \land k \in ℤ) \to O (C) \in ℕ_{0}$
113	112	nn0zd	$⊢ (φ \land k \in ℤ) \to O (C) \in ℤ$
114		hashcl	$⊢ B \in Fin \to \|B\| \in ℕ_{0}$
115	10 114	syl	$⊢ φ \to \|B\| \in ℕ_{0}$
116	115	nn0zd	$⊢ φ \to \|B\| \in ℤ$
117	116	adantr	$⊢ (φ \land k \in ℤ) \to \|B\| \in ℤ$
118	110 117	gcdcomd	$⊢ (φ \land k \in ℤ) \to (1 + k P) \gcd \|B\| = \|B\| \gcd (1 + k P)$
119	3	pgphash	$⊢ (P pGrp G \land B \in Fin) \to \|B\| = P^{P pCnt \|B\|}$
120	8 10 119	syl2anc	$⊢ φ \to \|B\| = P^{P pCnt \|B\|}$
121	120	adantr	$⊢ (φ \land k \in ℤ) \to \|B\| = P^{P pCnt \|B\|}$
122	121	oveq1d	$⊢ (φ \land k \in ℤ) \to \|B\| \gcd (1 + k P) = P^{P pCnt \|B\|} \gcd (1 + k P)$
123		simpr	$⊢ (φ \land k \in ℤ) \to k \in ℤ$
124	26	adantr	$⊢ (φ \land k \in ℤ) \to P \in ℤ$
125		1zzd	$⊢ (φ \land k \in ℤ) \to 1 \in ℤ$
126		gcdaddm	$⊢ (k \in ℤ \land P \in ℤ \land 1 \in ℤ) \to P \gcd 1 = P \gcd (1 + k P)$
127	123 124 125 126	syl3anc	$⊢ (φ \land k \in ℤ) \to P \gcd 1 = P \gcd (1 + k P)$
128		gcd1	$⊢ P \in ℤ \to P \gcd 1 = 1$
129	124 128	syl	$⊢ (φ \land k \in ℤ) \to P \gcd 1 = 1$
130	127 129	eqtr3d	$⊢ (φ \land k \in ℤ) \to P \gcd (1 + k P) = 1$
131	3	grpbn0	$⊢ G \in Grp \to B \neq \emptyset$
132	38 131	syl	$⊢ φ \to B \neq \emptyset$
133		hashnncl	$⊢ B \in Fin \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
134	10 133	syl	$⊢ φ \to (\|B\| \in ℕ \leftrightarrow B \neq \emptyset)$
135	132 134	mpbird	$⊢ φ \to \|B\| \in ℕ$
136	24 135	pccld	$⊢ φ \to P pCnt \|B\| \in ℕ_{0}$
137	136	adantr	$⊢ (φ \land k \in ℤ) \to P pCnt \|B\| \in ℕ_{0}$
138		rpexp1i	$⊢ (P \in ℤ \land 1 + k P \in ℤ \land P pCnt \|B\| \in ℕ_{0}) \to (P \gcd (1 + k P) = 1 \to P^{P pCnt \|B\|} \gcd (1 + k P) = 1)$
139	124 110 137 138	syl3anc	$⊢ (φ \land k \in ℤ) \to (P \gcd (1 + k P) = 1 \to P^{P pCnt \|B\|} \gcd (1 + k P) = 1)$
140	130 139	mpd	$⊢ (φ \land k \in ℤ) \to P^{P pCnt \|B\|} \gcd (1 + k P) = 1$
141	118 122 140	3eqtrd	$⊢ (φ \land k \in ℤ) \to (1 + k P) \gcd \|B\| = 1$
142	3 4	oddvds2	$⊢ (G \in Grp \land B \in Fin \land C \in B) \to O (C) ∥ \|B\|$
143	38 10 75 142	syl3anc	$⊢ φ \to O (C) ∥ \|B\|$
144	143	adantr	$⊢ (φ \land k \in ℤ) \to O (C) ∥ \|B\|$
145		rpdvds	$⊢ ((1 + k P \in ℤ \land O (C) \in ℤ \land \|B\| \in ℤ) \land ((1 + k P) \gcd \|B\| = 1 \land O (C) ∥ \|B\|)) \to (1 + k P) \gcd O (C) = 1$
146	110 113 117 141 144 145	syl32anc	$⊢ (φ \land k \in ℤ) \to (1 + k P) \gcd O (C) = 1$
147	3 4 19	odbezout	$⊢ ((G \in Grp \land C \in B \land 1 + k P \in ℤ) \land (1 + k P) \gcd O (C) = 1) \to \exists a \in ℤ a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) = C$
148	103 104 110 146 147	syl31anc	$⊢ (φ \land k \in ℤ) \to \exists a \in ℤ a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) = C$
149	49	ad2antrr	$⊢ ((φ \land k \in ℤ) \land a \in ℤ) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
150		simpr	$⊢ ((φ \land k \in ℤ) \land a \in ℤ) \to a \in ℤ$
151	19	subgmulgcl	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land a \in ℤ \land (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)) \to a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) \in (S \underset{˙}{\oplus} W)$
152	151	3expia	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land a \in ℤ) \to ((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) \in (S \underset{˙}{\oplus} W))$
153	149 150 152	syl2anc	$⊢ ((φ \land k \in ℤ) \land a \in ℤ) \to ((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) \in (S \underset{˙}{\oplus} W))$
154		eleq1	$⊢ a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) = C \to (a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) \in (S \underset{˙}{\oplus} W) \leftrightarrow C \in (S \underset{˙}{\oplus} W))$
155	154	imbi2d	$⊢ a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) = C \to (((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) \in (S \underset{˙}{\oplus} W)) \leftrightarrow ((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W)))$
156	153 155	syl5ibcom	$⊢ ((φ \land k \in ℤ) \land a \in ℤ) \to (a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) = C \to ((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W)))$
157	156	rexlimdva	$⊢ (φ \land k \in ℤ) \to (\exists a \in ℤ a \underset{˙}{\cdot} ((1 + k P) \underset{˙}{\cdot} C) = C \to ((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W)))$
158	148 157	mpd	$⊢ (φ \land k \in ℤ) \to ((1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W))$
159	158	rexlimdva	$⊢ φ \to (\exists k \in ℤ (1 + k P) \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W))$
160	102 159	syld	$⊢ φ \to (\neg P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W))$
161	20 160	mt3d	$⊢ φ \to P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)$

Metamath Proof Explorer

Theorem pgpfac1lem2

Proof