pgpfac1lem5

	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.3	$⊢ φ \to \forall s \in SubGrp (G) ((s \subset U \land A \in s) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s))$
Assertion	pgpfac1lem5	$⊢ φ \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.3	$⊢ φ \to \forall s \in SubGrp (G) ((s \subset U \land A \in s) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s))$
15		pwfi	$⊢ B \in Fin \leftrightarrow 𝒫 B \in Fin$
16	10 15	sylib	$⊢ φ \to 𝒫 B \in Fin$
17	16	adantr	$⊢ (φ \land S \subset U) \to 𝒫 B \in Fin$
18	3	subgss	$⊢ v \in SubGrp (G) \to v \subseteq B$
19	18	3ad2ant2	$⊢ ((φ \land S \subset U) \land v \in SubGrp (G) \land (v \subset U \land A \in v)) \to v \subseteq B$
20		velpw	$⊢ v \in 𝒫 B \leftrightarrow v \subseteq B$
21	19 20	sylibr	$⊢ ((φ \land S \subset U) \land v \in SubGrp (G) \land (v \subset U \land A \in v)) \to v \in 𝒫 B$
22	21	rabssdv	$⊢ (φ \land S \subset U) \to \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \subseteq 𝒫 B$
23	17 22	ssfid	$⊢ (φ \land S \subset U) \to \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \in Fin$
24		finnum	$⊢ \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \in Fin \to \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \in dom card$
25	23 24	syl	$⊢ (φ \land S \subset U) \to \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \in dom card$
26		ablgrp	$⊢ G \in Abel \to G \in Grp$
27	9 26	syl	$⊢ φ \to G \in Grp$
28	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (B)$
29		acsmre	$⊢ SubGrp (G) \in ACS (B) \to SubGrp (G) \in Moore (B)$
30	27 28 29	3syl	$⊢ φ \to SubGrp (G) \in Moore (B)$
31	3	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
32	12 31	syl	$⊢ φ \to U \subseteq B$
33	32 13	sseldd	$⊢ φ \to A \in B$
34	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land A \in B) \to K (\{A\}) \in SubGrp (G)$
35	30 33 34	syl2anc	$⊢ φ \to K (\{A\}) \in SubGrp (G)$
36	2 35	eqeltrid	$⊢ φ \to S \in SubGrp (G)$
37	36	adantr	$⊢ (φ \land S \subset U) \to S \in SubGrp (G)$
38		simpr	$⊢ (φ \land S \subset U) \to S \subset U$
39	13	snssd	$⊢ φ \to \{A\} \subseteq U$
40	39 32	sstrd	$⊢ φ \to \{A\} \subseteq B$
41	30 1 40	mrcssidd	$⊢ φ \to \{A\} \subseteq K (\{A\})$
42	41 2	sseqtrrdi	$⊢ φ \to \{A\} \subseteq S$
43		snssg	$⊢ A \in B \to (A \in S \leftrightarrow \{A\} \subseteq S)$
44	33 43	syl	$⊢ φ \to (A \in S \leftrightarrow \{A\} \subseteq S)$
45	42 44	mpbird	$⊢ φ \to A \in S$
46	45	adantr	$⊢ (φ \land S \subset U) \to A \in S$
47		psseq1	$⊢ v = S \to (v \subset U \leftrightarrow S \subset U)$
48		eleq2	$⊢ v = S \to (A \in v \leftrightarrow A \in S)$
49	47 48	anbi12d	$⊢ v = S \to ((v \subset U \land A \in v) \leftrightarrow (S \subset U \land A \in S))$
50	49	rspcev	$⊢ (S \in SubGrp (G) \land (S \subset U \land A \in S)) \to \exists v \in SubGrp (G) (v \subset U \land A \in v)$
51	37 38 46 50	syl12anc	$⊢ (φ \land S \subset U) \to \exists v \in SubGrp (G) (v \subset U \land A \in v)$
52		rabn0	$⊢ \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neq \emptyset \leftrightarrow \exists v \in SubGrp (G) (v \subset U \land A \in v)$
53	51 52	sylibr	$⊢ (φ \land S \subset U) \to \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neq \emptyset$
54		simpr1	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\}$
55		simpr2	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to u \neq \emptyset$
56	23	adantr	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \in Fin$
57	56 54	ssfid	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to u \in Fin$
58		simpr3	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to [\subset] Or u$
59		fin1a2lem10	$⊢ (u \neq \emptyset \land u \in Fin \land [\subset] Or u) \to ⋃ u \in u$
60	55 57 58 59	syl3anc	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to ⋃ u \in u$
61	54 60	sseldd	$⊢ ((φ \land S \subset U) \land (u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u)) \to ⋃ u \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\}$
62	61	ex	$⊢ (φ \land S \subset U) \to ((u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u) \to ⋃ u \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\})$
63	62	alrimiv	$⊢ (φ \land S \subset U) \to \forall u ((u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u) \to ⋃ u \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\})$
64		zornn0g	$⊢ (\{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \in dom card \land \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neq \emptyset \land \forall u ((u \subseteq \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \land u \neq \emptyset \land [\subset] Or u) \to ⋃ u \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\})) \to \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neg s \subset w$
65	25 53 63 64	syl3anc	$⊢ (φ \land S \subset U) \to \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neg s \subset w$
66		psseq1	$⊢ v = w \to (v \subset U \leftrightarrow w \subset U)$
67		eleq2	$⊢ v = w \to (A \in v \leftrightarrow A \in w)$
68	66 67	anbi12d	$⊢ v = w \to ((v \subset U \land A \in v) \leftrightarrow (w \subset U \land A \in w))$
69	68	ralrab	$⊢ \forall w \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neg s \subset w \leftrightarrow \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)$
70	69	rexbii	$⊢ \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \neg s \subset w \leftrightarrow \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)$
71	65 70	sylib	$⊢ (φ \land S \subset U) \to \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)$
72	71	ex	$⊢ φ \to (S \subset U \to \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))$
73		psseq1	$⊢ v = s \to (v \subset U \leftrightarrow s \subset U)$
74		eleq2	$⊢ v = s \to (A \in v \leftrightarrow A \in s)$
75	73 74	anbi12d	$⊢ v = s \to ((v \subset U \land A \in v) \leftrightarrow (s \subset U \land A \in s))$
76	75	ralrab	$⊢ \forall s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \leftrightarrow \forall s \in SubGrp (G) ((s \subset U \land A \in s) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s))$
77	14 76	sylibr	$⊢ φ \to \forall s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s)$
78		r19.29	$⊢ (\forall s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \land \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \to \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} (\exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))$
79	75	elrab	$⊢ s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \leftrightarrow (s \in SubGrp (G) \land (s \subset U \land A \in s))$
80		ineq2	$⊢ t = v \to S \cap t = S \cap v$
81	80	eqeq1d	$⊢ t = v \to (S \cap t = \{\underset{˙}{0}\} \leftrightarrow S \cap v = \{\underset{˙}{0}\})$
82		oveq2	$⊢ t = v \to S \underset{˙}{\oplus} t = S \underset{˙}{\oplus} v$
83	82	eqeq1d	$⊢ t = v \to (S \underset{˙}{\oplus} t = s \leftrightarrow S \underset{˙}{\oplus} v = s)$
84	81 83	anbi12d	$⊢ t = v \to ((S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \leftrightarrow (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s))$
85	84	cbvrexvw	$⊢ \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \leftrightarrow \exists v \in SubGrp (G) (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s)$
86		simprrl	$⊢ (φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \to s \subset U$
87	86	ad2antrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to s \subset U$
88		simpr2	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to S \underset{˙}{\oplus} v = s$
89	88	psseq1d	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to (S \underset{˙}{\oplus} v \subset U \leftrightarrow s \subset U)$
90	87 89	mpbird	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to S \underset{˙}{\oplus} v \subset U$
91		pssdif	$⊢ S \underset{˙}{\oplus} v \subset U \to U ∖ (S \underset{˙}{\oplus} v) \neq \emptyset$
92		n0	$⊢ U ∖ (S \underset{˙}{\oplus} v) \neq \emptyset \leftrightarrow \exists b b \in (U ∖ (S \underset{˙}{\oplus} v))$
93	91 92	sylib	$⊢ S \underset{˙}{\oplus} v \subset U \to \exists b b \in (U ∖ (S \underset{˙}{\oplus} v))$
94	90 93	syl	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to \exists b b \in (U ∖ (S \underset{˙}{\oplus} v))$
95	8	ad3antrrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to P pGrp G$
96	9	ad3antrrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to G \in Abel$
97	10	ad3antrrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to B \in Fin$
98	11	ad3antrrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to O (A) = E$
99	12	ad3antrrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to U \in SubGrp (G)$
100	13	ad3antrrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to A \in U$
101		simplr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to v \in SubGrp (G)$
102		simprl1	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to S \cap v = \{\underset{˙}{0}\}$
103	90	adantrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to S \underset{˙}{\oplus} v \subset U$
104	103	pssssd	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to S \underset{˙}{\oplus} v \subseteq U$
105		simprl3	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)$
106	88	adantrr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to S \underset{˙}{\oplus} v = s$
107		psseq1	$⊢ S \underset{˙}{\oplus} v = s \to (S \underset{˙}{\oplus} v \subset y \leftrightarrow s \subset y)$
108	107	notbid	$⊢ S \underset{˙}{\oplus} v = s \to (\neg S \underset{˙}{\oplus} v \subset y \leftrightarrow \neg s \subset y)$
109	108	imbi2d	$⊢ S \underset{˙}{\oplus} v = s \to (((y \subset U \land A \in y) \to \neg S \underset{˙}{\oplus} v \subset y) \leftrightarrow ((y \subset U \land A \in y) \to \neg s \subset y))$
110	109	ralbidv	$⊢ S \underset{˙}{\oplus} v = s \to (\forall y \in SubGrp (G) ((y \subset U \land A \in y) \to \neg S \underset{˙}{\oplus} v \subset y) \leftrightarrow \forall y \in SubGrp (G) ((y \subset U \land A \in y) \to \neg s \subset y))$
111		psseq1	$⊢ y = w \to (y \subset U \leftrightarrow w \subset U)$
112		eleq2	$⊢ y = w \to (A \in y \leftrightarrow A \in w)$
113	111 112	anbi12d	$⊢ y = w \to ((y \subset U \land A \in y) \leftrightarrow (w \subset U \land A \in w))$
114		psseq2	$⊢ y = w \to (s \subset y \leftrightarrow s \subset w)$
115	114	notbid	$⊢ y = w \to (\neg s \subset y \leftrightarrow \neg s \subset w)$
116	113 115	imbi12d	$⊢ y = w \to (((y \subset U \land A \in y) \to \neg s \subset y) \leftrightarrow ((w \subset U \land A \in w) \to \neg s \subset w))$
117	116	cbvralvw	$⊢ \forall y \in SubGrp (G) ((y \subset U \land A \in y) \to \neg s \subset y) \leftrightarrow \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)$
118	110 117	bitrdi	$⊢ S \underset{˙}{\oplus} v = s \to (\forall y \in SubGrp (G) ((y \subset U \land A \in y) \to \neg S \underset{˙}{\oplus} v \subset y) \leftrightarrow \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))$
119	106 118	syl	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to (\forall y \in SubGrp (G) ((y \subset U \land A \in y) \to \neg S \underset{˙}{\oplus} v \subset y) \leftrightarrow \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))$
120	105 119	mpbird	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to \forall y \in SubGrp (G) ((y \subset U \land A \in y) \to \neg S \underset{˙}{\oplus} v \subset y)$
121		simprr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to b \in (U ∖ (S \underset{˙}{\oplus} v))$
122		eqid	$⊢ \cdot_{G} = \cdot_{G}$
123	1 2 3 4 5 6 7 95 96 97 98 99 100 101 102 104 120 121 122	pgpfac1lem4	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \land b \in (U ∖ (S \underset{˙}{\oplus} v)))) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$
124	123	expr	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to (b \in (U ∖ (S \underset{˙}{\oplus} v)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
125	124	exlimdv	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to (\exists b b \in (U ∖ (S \underset{˙}{\oplus} v)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
126	94 125	mpd	$⊢ (((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \land (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w))) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$
127	126	3exp2	$⊢ ((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \to (S \cap v = \{\underset{˙}{0}\} \to (S \underset{˙}{\oplus} v = s \to (\forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))))$
128	127	impd	$⊢ ((φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \land v \in SubGrp (G)) \to ((S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s) \to (\forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)))$
129	128	rexlimdva	$⊢ (φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \to (\exists v \in SubGrp (G) (S \cap v = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} v = s) \to (\forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)))$
130	85 129	biimtrid	$⊢ (φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \to (\exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \to (\forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)))$
131	130	impd	$⊢ (φ \land (s \in SubGrp (G) \land (s \subset U \land A \in s))) \to ((\exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
132	79 131	sylan2b	$⊢ (φ \land s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\}) \to ((\exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
133	132	rexlimdva	$⊢ φ \to (\exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} (\exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \land \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
134	78 133	syl5	$⊢ φ \to ((\forall s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = s) \land \exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
135	77 134	mpand	$⊢ φ \to (\exists s \in \{v \in SubGrp (G) \| (v \subset U \land A \in v)\} \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg s \subset w) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
136	72 135	syld	$⊢ φ \to (S \subset U \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
137	6	0subg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in SubGrp (G)$
138	27 137	syl	$⊢ φ \to \{\underset{˙}{0}\} \in SubGrp (G)$
139	138	adantr	$⊢ (φ \land S = U) \to \{\underset{˙}{0}\} \in SubGrp (G)$
140	6	subg0cl	$⊢ S \in SubGrp (G) \to \underset{˙}{0} \in S$
141	36 140	syl	$⊢ φ \to \underset{˙}{0} \in S$
142	141	snssd	$⊢ φ \to \{\underset{˙}{0}\} \subseteq S$
143	142	adantr	$⊢ (φ \land S = U) \to \{\underset{˙}{0}\} \subseteq S$
144		sseqin2	$⊢ \{\underset{˙}{0}\} \subseteq S \leftrightarrow S \cap \{\underset{˙}{0}\} = \{\underset{˙}{0}\}$
145	143 144	sylib	$⊢ (φ \land S = U) \to S \cap \{\underset{˙}{0}\} = \{\underset{˙}{0}\}$
146	7	lsmss2	$⊢ (S \in SubGrp (G) \land \{\underset{˙}{0}\} \in SubGrp (G) \land \{\underset{˙}{0}\} \subseteq S) \to S \underset{˙}{\oplus} \{\underset{˙}{0}\} = S$
147	36 138 142 146	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} \{\underset{˙}{0}\} = S$
148	147	eqeq1d	$⊢ φ \to (S \underset{˙}{\oplus} \{\underset{˙}{0}\} = U \leftrightarrow S = U)$
149	148	biimpar	$⊢ (φ \land S = U) \to S \underset{˙}{\oplus} \{\underset{˙}{0}\} = U$
150		ineq2	$⊢ t = \{\underset{˙}{0}\} \to S \cap t = S \cap \{\underset{˙}{0}\}$
151	150	eqeq1d	$⊢ t = \{\underset{˙}{0}\} \to (S \cap t = \{\underset{˙}{0}\} \leftrightarrow S \cap \{\underset{˙}{0}\} = \{\underset{˙}{0}\})$
152		oveq2	$⊢ t = \{\underset{˙}{0}\} \to S \underset{˙}{\oplus} t = S \underset{˙}{\oplus} \{\underset{˙}{0}\}$
153	152	eqeq1d	$⊢ t = \{\underset{˙}{0}\} \to (S \underset{˙}{\oplus} t = U \leftrightarrow S \underset{˙}{\oplus} \{\underset{˙}{0}\} = U)$
154	151 153	anbi12d	$⊢ t = \{\underset{˙}{0}\} \to ((S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U) \leftrightarrow (S \cap \{\underset{˙}{0}\} = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} \{\underset{˙}{0}\} = U))$
155	154	rspcev	$⊢ (\{\underset{˙}{0}\} \in SubGrp (G) \land (S \cap \{\underset{˙}{0}\} = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} \{\underset{˙}{0}\} = U)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$
156	139 145 149 155	syl12anc	$⊢ (φ \land S = U) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$
157	156	ex	$⊢ φ \to (S = U \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U))$
158	1	mrcsscl	$⊢ (SubGrp (G) \in Moore (B) \land \{A\} \subseteq U \land U \in SubGrp (G)) \to K (\{A\}) \subseteq U$
159	30 39 12 158	syl3anc	$⊢ φ \to K (\{A\}) \subseteq U$
160	2 159	eqsstrid	$⊢ φ \to S \subseteq U$
161		sspss	$⊢ S \subseteq U \leftrightarrow (S \subset U \lor S = U)$
162	160 161	sylib	$⊢ φ \to (S \subset U \lor S = U)$
163	136 157 162	mpjaod	$⊢ φ \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$

Metamath Proof Explorer

Theorem pgpfac1lem5

Proof