pgpfac1lem3

	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$
	pgpfac1.d	$⊢ D = C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)$
Assertion	pgpfac1lem3	$⊢ φ \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$

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		pgpfac1.d	$⊢ D = C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)$
23		ablgrp	$⊢ G \in Abel \to G \in Grp$
24	9 23	syl	$⊢ φ \to G \in Grp$
25	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (B)$
26		acsmre	$⊢ SubGrp (G) \in ACS (B) \to SubGrp (G) \in Moore (B)$
27	24 25 26	3syl	$⊢ φ \to SubGrp (G) \in Moore (B)$
28	3	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
29	12 28	syl	$⊢ φ \to U \subseteq B$
30	18	eldifad	$⊢ φ \to C \in U$
31	29 13	sseldd	$⊢ φ \to A \in B$
32	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land A \in B) \to K (\{A\}) \in SubGrp (G)$
33	27 31 32	syl2anc	$⊢ φ \to K (\{A\}) \in SubGrp (G)$
34	2 33	eqeltrid	$⊢ φ \to S \in SubGrp (G)$
35	7	lsmub1	$⊢ (S \in SubGrp (G) \land W \in SubGrp (G)) \to S \subseteq S \underset{˙}{\oplus} W$
36	34 14 35	syl2anc	$⊢ φ \to S \subseteq S \underset{˙}{\oplus} W$
37	36 16	sstrd	$⊢ φ \to S \subseteq U$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21	pgpfac1lem3a	$⊢ φ \to (P ∥ E \land P ∥ M)$
39	38	simprd	$⊢ φ \to P ∥ M$
40		pgpprm	$⊢ P pGrp G \to P \in ℙ$
41	8 40	syl	$⊢ φ \to P \in ℙ$
42		prmz	$⊢ P \in ℙ \to P \in ℤ$
43	41 42	syl	$⊢ φ \to P \in ℤ$
44		prmnn	$⊢ P \in ℙ \to P \in ℕ$
45	41 44	syl	$⊢ φ \to P \in ℕ$
46	45	nnne0d	$⊢ φ \to P \neq 0$
47		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land M \in ℤ) \to (P ∥ M \leftrightarrow \frac{M}{P} \in ℤ)$
48	43 46 20 47	syl3anc	$⊢ φ \to (P ∥ M \leftrightarrow \frac{M}{P} \in ℤ)$
49	39 48	mpbid	$⊢ φ \to \frac{M}{P} \in ℤ$
50	31	snssd	$⊢ φ \to \{A\} \subseteq B$
51	27 1 50	mrcssidd	$⊢ φ \to \{A\} \subseteq K (\{A\})$
52	51 2	sseqtrrdi	$⊢ φ \to \{A\} \subseteq S$
53		snssg	$⊢ A \in U \to (A \in S \leftrightarrow \{A\} \subseteq S)$
54	13 53	syl	$⊢ φ \to (A \in S \leftrightarrow \{A\} \subseteq S)$
55	52 54	mpbird	$⊢ φ \to A \in S$
56	19	subgmulgcl	$⊢ (S \in SubGrp (G) \land \frac{M}{P} \in ℤ \land A \in S) \to (\frac{M}{P}) \underset{˙}{\cdot} A \in S$
57	34 49 55 56	syl3anc	$⊢ φ \to (\frac{M}{P}) \underset{˙}{\cdot} A \in S$
58	37 57	sseldd	$⊢ φ \to (\frac{M}{P}) \underset{˙}{\cdot} A \in U$
59		eqid	$⊢ +_{G} = +_{G}$
60	59	subgcl	$⊢ (U \in SubGrp (G) \land C \in U \land (\frac{M}{P}) \underset{˙}{\cdot} A \in U) \to C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in U$
61	12 30 58 60	syl3anc	$⊢ φ \to C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in U$
62	22 61	eqeltrid	$⊢ φ \to D \in U$
63	29 62	sseldd	$⊢ φ \to D \in B$
64	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land D \in B) \to K (\{D\}) \in SubGrp (G)$
65	27 63 64	syl2anc	$⊢ φ \to K (\{D\}) \in SubGrp (G)$
66	7	lsmsubg2	$⊢ (G \in Abel \land W \in SubGrp (G) \land K (\{D\}) \in SubGrp (G)) \to W \underset{˙}{\oplus} K (\{D\}) \in SubGrp (G)$
67	9 14 65 66	syl3anc	$⊢ φ \to W \underset{˙}{\oplus} K (\{D\}) \in SubGrp (G)$
68		eqid	$⊢ -_{G} = -_{G}$
69	68 7 14 65	lsmelvalm	$⊢ φ \to (x \in (W \underset{˙}{\oplus} K (\{D\})) \leftrightarrow \exists w \in W \exists y \in K (\{D\}) x = w -_{G} y)$
70		eqid	$⊢ (n \in ℤ ⟼ n \underset{˙}{\cdot} D) = (n \in ℤ ⟼ n \underset{˙}{\cdot} D)$
71	3 19 70 1	cycsubg2	$⊢ (G \in Grp \land D \in B) \to K (\{D\}) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} D)$
72	24 63 71	syl2anc	$⊢ φ \to K (\{D\}) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} D)$
73	72	rexeqdv	$⊢ φ \to (\exists y \in K (\{D\}) x = w -_{G} y \leftrightarrow \exists y \in ran (n \in ℤ ⟼ n \underset{˙}{\cdot} D) x = w -_{G} y)$
74		ovex	$⊢ n \underset{˙}{\cdot} D \in V$
75	74	rgenw	$⊢ \forall n \in ℤ n \underset{˙}{\cdot} D \in V$
76		oveq2	$⊢ y = n \underset{˙}{\cdot} D \to w -_{G} y = w -_{G} (n \underset{˙}{\cdot} D)$
77	76	eqeq2d	$⊢ y = n \underset{˙}{\cdot} D \to (x = w -_{G} y \leftrightarrow x = w -_{G} (n \underset{˙}{\cdot} D))$
78	70 77	rexrnmptw	$⊢ \forall n \in ℤ n \underset{˙}{\cdot} D \in V \to (\exists y \in ran (n \in ℤ ⟼ n \underset{˙}{\cdot} D) x = w -_{G} y \leftrightarrow \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D))$
79	75 78	ax-mp	$⊢ \exists y \in ran (n \in ℤ ⟼ n \underset{˙}{\cdot} D) x = w -_{G} y \leftrightarrow \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D)$
80	73 79	bitrdi	$⊢ φ \to (\exists y \in K (\{D\}) x = w -_{G} y \leftrightarrow \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D))$
81	80	rexbidv	$⊢ φ \to (\exists w \in W \exists y \in K (\{D\}) x = w -_{G} y \leftrightarrow \exists w \in W \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D))$
82	69 81	bitrd	$⊢ φ \to (x \in (W \underset{˙}{\oplus} K (\{D\})) \leftrightarrow \exists w \in W \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D))$
83	82	adantr	$⊢ (φ \land x \in S) \to (x \in (W \underset{˙}{\oplus} K (\{D\})) \leftrightarrow \exists w \in W \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D))$
84		simpr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to x = w -_{G} (n \underset{˙}{\cdot} D)$
85	14	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to W \in SubGrp (G)$
86		simplrl	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w \in W$
87		simplrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to n \in ℤ$
88	87	zcnd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to n \in ℂ$
89	45	nncnd	$⊢ φ \to P \in ℂ$
90	89	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P \in ℂ$
91	46	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P \neq 0$
92	88 90 91	divcan1d	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\frac{n}{P}) P = n$
93	92	oveq1d	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\frac{n}{P}) P \underset{˙}{\cdot} D = n \underset{˙}{\cdot} D$
94	24	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to G \in Grp$
95	18	eldifbd	$⊢ φ \to \neg C \in (S \underset{˙}{\oplus} W)$
96	7	lsmsubg2	$⊢ (G \in Abel \land S \in SubGrp (G) \land W \in SubGrp (G)) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
97	9 34 14 96	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} W \in SubGrp (G)$
98	36 57	sseldd	$⊢ φ \to (\frac{M}{P}) \underset{˙}{\cdot} A \in (S \underset{˙}{\oplus} W)$
99	68	subgsubcl	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land D \in (S \underset{˙}{\oplus} W) \land (\frac{M}{P}) \underset{˙}{\cdot} A \in (S \underset{˙}{\oplus} W)) \to D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in (S \underset{˙}{\oplus} W)$
100	99	3expia	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land D \in (S \underset{˙}{\oplus} W)) \to ((\frac{M}{P}) \underset{˙}{\cdot} A \in (S \underset{˙}{\oplus} W) \to D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in (S \underset{˙}{\oplus} W))$
101	100	impancom	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land (\frac{M}{P}) \underset{˙}{\cdot} A \in (S \underset{˙}{\oplus} W)) \to (D \in (S \underset{˙}{\oplus} W) \to D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in (S \underset{˙}{\oplus} W))$
102	97 98 101	syl2anc	$⊢ φ \to (D \in (S \underset{˙}{\oplus} W) \to D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in (S \underset{˙}{\oplus} W))$
103	22	oveq1i	$⊢ D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) = (C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)) -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)$
104	29 30	sseldd	$⊢ φ \to C \in B$
105	3	subgss	$⊢ S \in SubGrp (G) \to S \subseteq B$
106	34 105	syl	$⊢ φ \to S \subseteq B$
107	106 57	sseldd	$⊢ φ \to (\frac{M}{P}) \underset{˙}{\cdot} A \in B$
108	3 59 68	grppncan	$⊢ (G \in Grp \land C \in B \land (\frac{M}{P}) \underset{˙}{\cdot} A \in B) \to (C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)) -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) = C$
109	24 104 107 108	syl3anc	$⊢ φ \to (C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)) -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) = C$
110	103 109	eqtrid	$⊢ φ \to D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) = C$
111	110	eleq1d	$⊢ φ \to (D -_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A) \in (S \underset{˙}{\oplus} W) \leftrightarrow C \in (S \underset{˙}{\oplus} W))$
112	102 111	sylibd	$⊢ φ \to (D \in (S \underset{˙}{\oplus} W) \to C \in (S \underset{˙}{\oplus} W))$
113	95 112	mtod	$⊢ φ \to \neg D \in (S \underset{˙}{\oplus} W)$
114	113	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to \neg D \in (S \underset{˙}{\oplus} W)$
115	41	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P \in ℙ$
116		coprm	$⊢ (P \in ℙ \land n \in ℤ) \to (\neg P ∥ n \leftrightarrow P \gcd n = 1)$
117	115 87 116	syl2anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\neg P ∥ n \leftrightarrow P \gcd n = 1)$
118	43	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P \in ℤ$
119		bezout	$⊢ (P \in ℤ \land n \in ℤ) \to \exists a \in ℤ \exists b \in ℤ P \gcd n = P a + n b$
120	118 87 119	syl2anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to \exists a \in ℤ \exists b \in ℤ P \gcd n = P a + n b$
121		eqeq1	$⊢ P \gcd n = 1 \to (P \gcd n = P a + n b \leftrightarrow 1 = P a + n b)$
122	121	2rexbidv	$⊢ P \gcd n = 1 \to (\exists a \in ℤ \exists b \in ℤ P \gcd n = P a + n b \leftrightarrow \exists a \in ℤ \exists b \in ℤ 1 = P a + n b)$
123	120 122	syl5ibcom	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (P \gcd n = 1 \to \exists a \in ℤ \exists b \in ℤ 1 = P a + n b)$
124	94	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to G \in Grp$
125	118	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P \in ℤ$
126		simprl	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
127	125 126	zmulcld	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P a \in ℤ$
128	87	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n \in ℤ$
129		simprr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
130	128 129	zmulcld	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n b \in ℤ$
131	63	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to D \in B$
132	131	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to D \in B$
133	3 19 59	mulgdir	$⊢ (G \in Grp \land (P a \in ℤ \land n b \in ℤ \land D \in B)) \to (P a + n b) \underset{˙}{\cdot} D = (P a \underset{˙}{\cdot} D) +_{G} (n b \underset{˙}{\cdot} D)$
134	124 127 130 132 133	syl13anc	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to (P a + n b) \underset{˙}{\cdot} D = (P a \underset{˙}{\cdot} D) +_{G} (n b \underset{˙}{\cdot} D)$
135	97	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
136	135	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to S \underset{˙}{\oplus} W \in SubGrp (G)$
137	90	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P \in ℂ$
138		zcn	$⊢ a \in ℤ \to a \in ℂ$
139	138	ad2antrl	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to a \in ℂ$
140	137 139	mulcomd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P a = a P$
141	140	oveq1d	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P a \underset{˙}{\cdot} D = a P \underset{˙}{\cdot} D$
142	3 19	mulgass	$⊢ (G \in Grp \land (a \in ℤ \land P \in ℤ \land D \in B)) \to a P \underset{˙}{\cdot} D = a \underset{˙}{\cdot} (P \underset{˙}{\cdot} D)$
143	124 126 125 132 142	syl13anc	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to a P \underset{˙}{\cdot} D = a \underset{˙}{\cdot} (P \underset{˙}{\cdot} D)$
144	141 143	eqtrd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P a \underset{˙}{\cdot} D = a \underset{˙}{\cdot} (P \underset{˙}{\cdot} D)$
145	7	lsmub2	$⊢ (S \in SubGrp (G) \land W \in SubGrp (G)) \to W \subseteq S \underset{˙}{\oplus} W$
146	34 14 145	syl2anc	$⊢ φ \to W \subseteq S \underset{˙}{\oplus} W$
147	22	oveq2i	$⊢ P \underset{˙}{\cdot} D = P \underset{˙}{\cdot} (C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A))$
148	3 19 59	mulgdi	$⊢ (G \in Abel \land (P \in ℤ \land C \in B \land (\frac{M}{P}) \underset{˙}{\cdot} A \in B)) \to P \underset{˙}{\cdot} (C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)) = (P \underset{˙}{\cdot} C) +_{G} (P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A))$
149	9 43 104 107 148	syl13anc	$⊢ φ \to P \underset{˙}{\cdot} (C +_{G} ((\frac{M}{P}) \underset{˙}{\cdot} A)) = (P \underset{˙}{\cdot} C) +_{G} (P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A))$
150	147 149	eqtrid	$⊢ φ \to P \underset{˙}{\cdot} D = (P \underset{˙}{\cdot} C) +_{G} (P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A))$
151	3 19	mulgass	$⊢ (G \in Grp \land (P \in ℤ \land \frac{M}{P} \in ℤ \land A \in B)) \to P (\frac{M}{P}) \underset{˙}{\cdot} A = P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A)$
152	24 43 49 31 151	syl13anc	$⊢ φ \to P (\frac{M}{P}) \underset{˙}{\cdot} A = P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A)$
153	20	zcnd	$⊢ φ \to M \in ℂ$
154	153 89 46	divcan2d	$⊢ φ \to P (\frac{M}{P}) = M$
155	154	oveq1d	$⊢ φ \to P (\frac{M}{P}) \underset{˙}{\cdot} A = M \underset{˙}{\cdot} A$
156	152 155	eqtr3d	$⊢ φ \to P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A) = M \underset{˙}{\cdot} A$
157	156	oveq2d	$⊢ φ \to (P \underset{˙}{\cdot} C) +_{G} (P \underset{˙}{\cdot} ((\frac{M}{P}) \underset{˙}{\cdot} A)) = (P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)$
158	150 157	eqtrd	$⊢ φ \to P \underset{˙}{\cdot} D = (P \underset{˙}{\cdot} C) +_{G} (M \underset{˙}{\cdot} A)$
159	158 21	eqeltrd	$⊢ φ \to P \underset{˙}{\cdot} D \in W$
160	146 159	sseldd	$⊢ φ \to P \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
161	160	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
162	161	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
163	19	subgmulgcl	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land a \in ℤ \land P \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)) \to a \underset{˙}{\cdot} (P \underset{˙}{\cdot} D) \in (S \underset{˙}{\oplus} W)$
164	136 126 162 163	syl3anc	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to a \underset{˙}{\cdot} (P \underset{˙}{\cdot} D) \in (S \underset{˙}{\oplus} W)$
165	144 164	eqeltrd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to P a \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
166	88	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n \in ℂ$
167		zcn	$⊢ b \in ℤ \to b \in ℂ$
168	167	ad2antll	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to b \in ℂ$
169	166 168	mulcomd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n b = b n$
170	169	oveq1d	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n b \underset{˙}{\cdot} D = b n \underset{˙}{\cdot} D$
171	3 19	mulgass	$⊢ (G \in Grp \land (b \in ℤ \land n \in ℤ \land D \in B)) \to b n \underset{˙}{\cdot} D = b \underset{˙}{\cdot} (n \underset{˙}{\cdot} D)$
172	124 129 128 132 171	syl13anc	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to b n \underset{˙}{\cdot} D = b \underset{˙}{\cdot} (n \underset{˙}{\cdot} D)$
173	170 172	eqtrd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n b \underset{˙}{\cdot} D = b \underset{˙}{\cdot} (n \underset{˙}{\cdot} D)$
174	84	oveq2d	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w -_{G} x = w -_{G} (w -_{G} (n \underset{˙}{\cdot} D))$
175	9	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to G \in Abel$
176	3	subgss	$⊢ W \in SubGrp (G) \to W \subseteq B$
177	85 176	syl	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to W \subseteq B$
178	177 86	sseldd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w \in B$
179	3 19	mulgcl	$⊢ (G \in Grp \land n \in ℤ \land D \in B) \to n \underset{˙}{\cdot} D \in B$
180	94 87 131 179	syl3anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to n \underset{˙}{\cdot} D \in B$
181	3 68 175 178 180	ablnncan	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w -_{G} (w -_{G} (n \underset{˙}{\cdot} D)) = n \underset{˙}{\cdot} D$
182	174 181	eqtrd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w -_{G} x = n \underset{˙}{\cdot} D$
183	146	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to W \subseteq S \underset{˙}{\oplus} W$
184	183 86	sseldd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w \in (S \underset{˙}{\oplus} W)$
185	36	sselda	$⊢ (φ \land x \in S) \to x \in (S \underset{˙}{\oplus} W)$
186	185	ad2antrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to x \in (S \underset{˙}{\oplus} W)$
187	68	subgsubcl	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land w \in (S \underset{˙}{\oplus} W) \land x \in (S \underset{˙}{\oplus} W)) \to w -_{G} x \in (S \underset{˙}{\oplus} W)$
188	135 184 186 187	syl3anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w -_{G} x \in (S \underset{˙}{\oplus} W)$
189	182 188	eqeltrrd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to n \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
190	189	adantr	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
191	19	subgmulgcl	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land b \in ℤ \land n \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)) \to b \underset{˙}{\cdot} (n \underset{˙}{\cdot} D) \in (S \underset{˙}{\oplus} W)$
192	136 129 190 191	syl3anc	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to b \underset{˙}{\cdot} (n \underset{˙}{\cdot} D) \in (S \underset{˙}{\oplus} W)$
193	173 192	eqeltrd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to n b \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
194	59	subgcl	$⊢ (S \underset{˙}{\oplus} W \in SubGrp (G) \land P a \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W) \land n b \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)) \to (P a \underset{˙}{\cdot} D) +_{G} (n b \underset{˙}{\cdot} D) \in (S \underset{˙}{\oplus} W)$
195	136 165 193 194	syl3anc	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to (P a \underset{˙}{\cdot} D) +_{G} (n b \underset{˙}{\cdot} D) \in (S \underset{˙}{\oplus} W)$
196	134 195	eqeltrd	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to (P a + n b) \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W)$
197		oveq1	$⊢ 1 = P a + n b \to 1 \underset{˙}{\cdot} D = (P a + n b) \underset{˙}{\cdot} D$
198	197	eleq1d	$⊢ 1 = P a + n b \to (1 \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W) \leftrightarrow (P a + n b) \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W))$
199	196 198	syl5ibrcom	$⊢ ((((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \land (a \in ℤ \land b \in ℤ)) \to (1 = P a + n b \to 1 \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W))$
200	199	rexlimdvva	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\exists a \in ℤ \exists b \in ℤ 1 = P a + n b \to 1 \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W))$
201	123 200	syld	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (P \gcd n = 1 \to 1 \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W))$
202	3 19	mulg1	$⊢ D \in B \to 1 \underset{˙}{\cdot} D = D$
203	131 202	syl	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to 1 \underset{˙}{\cdot} D = D$
204	203	eleq1d	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (1 \underset{˙}{\cdot} D \in (S \underset{˙}{\oplus} W) \leftrightarrow D \in (S \underset{˙}{\oplus} W))$
205	201 204	sylibd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (P \gcd n = 1 \to D \in (S \underset{˙}{\oplus} W))$
206	117 205	sylbid	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\neg P ∥ n \to D \in (S \underset{˙}{\oplus} W))$
207	114 206	mt3d	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P ∥ n$
208		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land n \in ℤ) \to (P ∥ n \leftrightarrow \frac{n}{P} \in ℤ)$
209	118 91 87 208	syl3anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (P ∥ n \leftrightarrow \frac{n}{P} \in ℤ)$
210	207 209	mpbid	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to \frac{n}{P} \in ℤ$
211	3 19	mulgass	$⊢ (G \in Grp \land (\frac{n}{P} \in ℤ \land P \in ℤ \land D \in B)) \to (\frac{n}{P}) P \underset{˙}{\cdot} D = (\frac{n}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} D)$
212	94 210 118 131 211	syl13anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\frac{n}{P}) P \underset{˙}{\cdot} D = (\frac{n}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} D)$
213	93 212	eqtr3d	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to n \underset{˙}{\cdot} D = (\frac{n}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} D)$
214	159	ad3antrrr	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to P \underset{˙}{\cdot} D \in W$
215	19	subgmulgcl	$⊢ (W \in SubGrp (G) \land \frac{n}{P} \in ℤ \land P \underset{˙}{\cdot} D \in W) \to (\frac{n}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} D) \in W$
216	85 210 214 215	syl3anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to (\frac{n}{P}) \underset{˙}{\cdot} (P \underset{˙}{\cdot} D) \in W$
217	213 216	eqeltrd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to n \underset{˙}{\cdot} D \in W$
218	68	subgsubcl	$⊢ (W \in SubGrp (G) \land w \in W \land n \underset{˙}{\cdot} D \in W) \to w -_{G} (n \underset{˙}{\cdot} D) \in W$
219	85 86 217 218	syl3anc	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to w -_{G} (n \underset{˙}{\cdot} D) \in W$
220	84 219	eqeltrd	$⊢ (((φ \land x \in S) \land (w \in W \land n \in ℤ)) \land x = w -_{G} (n \underset{˙}{\cdot} D)) \to x \in W$
221	220	ex	$⊢ ((φ \land x \in S) \land (w \in W \land n \in ℤ)) \to (x = w -_{G} (n \underset{˙}{\cdot} D) \to x \in W)$
222	221	rexlimdvva	$⊢ (φ \land x \in S) \to (\exists w \in W \exists n \in ℤ x = w -_{G} (n \underset{˙}{\cdot} D) \to x \in W)$
223	83 222	sylbid	$⊢ (φ \land x \in S) \to (x \in (W \underset{˙}{\oplus} K (\{D\})) \to x \in W)$
224	223	imdistanda	$⊢ φ \to ((x \in S \land x \in (W \underset{˙}{\oplus} K (\{D\}))) \to (x \in S \land x \in W))$
225		elin	$⊢ x \in (S \cap (W \underset{˙}{\oplus} K (\{D\}))) \leftrightarrow (x \in S \land x \in (W \underset{˙}{\oplus} K (\{D\})))$
226		elin	$⊢ x \in (S \cap W) \leftrightarrow (x \in S \land x \in W)$
227	224 225 226	3imtr4g	$⊢ φ \to (x \in (S \cap (W \underset{˙}{\oplus} K (\{D\}))) \to x \in (S \cap W))$
228	227	ssrdv	$⊢ φ \to S \cap (W \underset{˙}{\oplus} K (\{D\})) \subseteq S \cap W$
229	228 15	sseqtrd	$⊢ φ \to S \cap (W \underset{˙}{\oplus} K (\{D\})) \subseteq \{\underset{˙}{0}\}$
230	6	subg0cl	$⊢ S \in SubGrp (G) \to \underset{˙}{0} \in S$
231	34 230	syl	$⊢ φ \to \underset{˙}{0} \in S$
232	6	subg0cl	$⊢ W \underset{˙}{\oplus} K (\{D\}) \in SubGrp (G) \to \underset{˙}{0} \in (W \underset{˙}{\oplus} K (\{D\}))$
233	67 232	syl	$⊢ φ \to \underset{˙}{0} \in (W \underset{˙}{\oplus} K (\{D\}))$
234	231 233	elind	$⊢ φ \to \underset{˙}{0} \in (S \cap (W \underset{˙}{\oplus} K (\{D\})))$
235	234	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq S \cap (W \underset{˙}{\oplus} K (\{D\}))$
236	229 235	eqssd	$⊢ φ \to S \cap (W \underset{˙}{\oplus} K (\{D\})) = \{\underset{˙}{0}\}$
237	7	lsmass	$⊢ (S \in SubGrp (G) \land W \in SubGrp (G) \land K (\{D\}) \in SubGrp (G)) \to (S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{D\}) = S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\}))$
238	34 14 65 237	syl3anc	$⊢ φ \to (S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{D\}) = S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\}))$
239	62 113	eldifd	$⊢ φ \to D \in (U ∖ (S \underset{˙}{\oplus} W))$
240	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17	pgpfac1lem1	$⊢ (φ \land D \in (U ∖ (S \underset{˙}{\oplus} W))) \to (S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{D\}) = U$
241	239 240	mpdan	$⊢ φ \to (S \underset{˙}{\oplus} W) \underset{˙}{\oplus} K (\{D\}) = U$
242	238 241	eqtr3d	$⊢ φ \to S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\})) = U$
243		ineq2	$⊢ t = W \underset{˙}{\oplus} K (\{D\}) \to S \cap t = S \cap (W \underset{˙}{\oplus} K (\{D\}))$
244	243	eqeq1d	$⊢ t = W \underset{˙}{\oplus} K (\{D\}) \to (S \cap t = \{\underset{˙}{0}\} \leftrightarrow S \cap (W \underset{˙}{\oplus} K (\{D\})) = \{\underset{˙}{0}\})$
245		oveq2	$⊢ t = W \underset{˙}{\oplus} K (\{D\}) \to S \underset{˙}{\oplus} t = S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\}))$
246	245	eqeq1d	$⊢ t = W \underset{˙}{\oplus} K (\{D\}) \to (S \underset{˙}{\oplus} t = U \leftrightarrow S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\})) = U)$
247	244 246	anbi12d	$⊢ t = W \underset{˙}{\oplus} K (\{D\}) \to ((S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U) \leftrightarrow (S \cap (W \underset{˙}{\oplus} K (\{D\})) = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\})) = U))$
248	247	rspcev	$⊢ (W \underset{˙}{\oplus} K (\{D\}) \in SubGrp (G) \land (S \cap (W \underset{˙}{\oplus} K (\{D\})) = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} (W \underset{˙}{\oplus} K (\{D\})) = U)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$
249	67 236 242 248	syl12anc	$⊢ φ \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$

Metamath Proof Explorer

Theorem pgpfac1lem3

Proof