pgpfac1lem4

	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	pgpfac1lem4	$⊢ φ \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	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19	pgpfac1lem2	$⊢ φ \to P \underset{˙}{\cdot} C \in (S \underset{˙}{\oplus} W)$
21		ablgrp	$⊢ G \in Abel \to G \in Grp$
22	9 21	syl	$⊢ φ \to G \in Grp$
23	3	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (B)$
24		acsmre	$⊢ SubGrp (G) \in ACS (B) \to SubGrp (G) \in Moore (B)$
25	22 23 24	3syl	$⊢ φ \to SubGrp (G) \in Moore (B)$
26	3	subgss	$⊢ U \in SubGrp (G) \to U \subseteq B$
27	12 26	syl	$⊢ φ \to U \subseteq B$
28	27 13	sseldd	$⊢ φ \to A \in B$
29	1	mrcsncl	$⊢ (SubGrp (G) \in Moore (B) \land A \in B) \to K (\{A\}) \in SubGrp (G)$
30	25 28 29	syl2anc	$⊢ φ \to K (\{A\}) \in SubGrp (G)$
31	2 30	eqeltrid	$⊢ φ \to S \in SubGrp (G)$
32	7	lsmcom	$⊢ (G \in Abel \land S \in SubGrp (G) \land W \in SubGrp (G)) \to S \underset{˙}{\oplus} W = W \underset{˙}{\oplus} S$
33	9 31 14 32	syl3anc	$⊢ φ \to S \underset{˙}{\oplus} W = W \underset{˙}{\oplus} S$
34	20 33	eleqtrd	$⊢ φ \to P \underset{˙}{\cdot} C \in (W \underset{˙}{\oplus} S)$
35		eqid	$⊢ -_{G} = -_{G}$
36	35 7 14 31	lsmelvalm	$⊢ φ \to (P \underset{˙}{\cdot} C \in (W \underset{˙}{\oplus} S) \leftrightarrow \exists w \in W \exists s \in S P \underset{˙}{\cdot} C = w -_{G} s)$
37	34 36	mpbid	$⊢ φ \to \exists w \in W \exists s \in S P \underset{˙}{\cdot} C = w -_{G} s$
38		eqid	$⊢ (k \in ℤ ⟼ k \underset{˙}{\cdot} A) = (k \in ℤ ⟼ k \underset{˙}{\cdot} A)$
39	3 19 38 1	cycsubg2	$⊢ (G \in Grp \land A \in B) \to K (\{A\}) = ran (k \in ℤ ⟼ k \underset{˙}{\cdot} A)$
40	22 28 39	syl2anc	$⊢ φ \to K (\{A\}) = ran (k \in ℤ ⟼ k \underset{˙}{\cdot} A)$
41	2 40	syl5eq	$⊢ φ \to S = ran (k \in ℤ ⟼ k \underset{˙}{\cdot} A)$
42	41	rexeqdv	$⊢ φ \to (\exists s \in S P \underset{˙}{\cdot} C = w -_{G} s \leftrightarrow \exists s \in ran (k \in ℤ ⟼ k \underset{˙}{\cdot} A) P \underset{˙}{\cdot} C = w -_{G} s)$
43		ovex	$⊢ k \underset{˙}{\cdot} A \in V$
44	43	rgenw	$⊢ \forall k \in ℤ k \underset{˙}{\cdot} A \in V$
45		oveq2	$⊢ s = k \underset{˙}{\cdot} A \to w -_{G} s = w -_{G} (k \underset{˙}{\cdot} A)$
46	45	eqeq2d	$⊢ s = k \underset{˙}{\cdot} A \to (P \underset{˙}{\cdot} C = w -_{G} s \leftrightarrow P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A))$
47	38 46	rexrnmptw	$⊢ \forall k \in ℤ k \underset{˙}{\cdot} A \in V \to (\exists s \in ran (k \in ℤ ⟼ k \underset{˙}{\cdot} A) P \underset{˙}{\cdot} C = w -_{G} s \leftrightarrow \exists k \in ℤ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A))$
48	44 47	ax-mp	$⊢ \exists s \in ran (k \in ℤ ⟼ k \underset{˙}{\cdot} A) P \underset{˙}{\cdot} C = w -_{G} s \leftrightarrow \exists k \in ℤ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A)$
49	42 48	bitrdi	$⊢ φ \to (\exists s \in S P \underset{˙}{\cdot} C = w -_{G} s \leftrightarrow \exists k \in ℤ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A))$
50	49	rexbidv	$⊢ φ \to (\exists w \in W \exists s \in S P \underset{˙}{\cdot} C = w -_{G} s \leftrightarrow \exists w \in W \exists k \in ℤ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A))$
51	37 50	mpbid	$⊢ φ \to \exists w \in W \exists k \in ℤ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A)$
52		rexcom	$⊢ \exists w \in W \exists k \in ℤ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A) \leftrightarrow \exists k \in ℤ \exists w \in W P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A)$
53	51 52	sylib	$⊢ φ \to \exists k \in ℤ \exists w \in W P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A)$
54	22	ad2antrr	$⊢ ((φ \land k \in ℤ) \land w \in W) \to G \in Grp$
55	3	subgss	$⊢ W \in SubGrp (G) \to W \subseteq B$
56	14 55	syl	$⊢ φ \to W \subseteq B$
57	56	adantr	$⊢ (φ \land k \in ℤ) \to W \subseteq B$
58	57	sselda	$⊢ ((φ \land k \in ℤ) \land w \in W) \to w \in B$
59		simplr	$⊢ ((φ \land k \in ℤ) \land w \in W) \to k \in ℤ$
60	28	ad2antrr	$⊢ ((φ \land k \in ℤ) \land w \in W) \to A \in B$
61	3 19	mulgcl	$⊢ (G \in Grp \land k \in ℤ \land A \in B) \to k \underset{˙}{\cdot} A \in B$
62	54 59 60 61	syl3anc	$⊢ ((φ \land k \in ℤ) \land w \in W) \to k \underset{˙}{\cdot} A \in B$
63		pgpprm	$⊢ P pGrp G \to P \in ℙ$
64		prmz	$⊢ P \in ℙ \to P \in ℤ$
65	8 63 64	3syl	$⊢ φ \to P \in ℤ$
66	18	eldifad	$⊢ φ \to C \in U$
67	27 66	sseldd	$⊢ φ \to C \in B$
68	3 19	mulgcl	$⊢ (G \in Grp \land P \in ℤ \land C \in B) \to P \underset{˙}{\cdot} C \in B$
69	22 65 67 68	syl3anc	$⊢ φ \to P \underset{˙}{\cdot} C \in B$
70	69	ad2antrr	$⊢ ((φ \land k \in ℤ) \land w \in W) \to P \underset{˙}{\cdot} C \in B$
71		eqid	$⊢ +_{G} = +_{G}$
72	3 71 35	grpsubadd	$⊢ (G \in Grp \land (w \in B \land k \underset{˙}{\cdot} A \in B \land P \underset{˙}{\cdot} C \in B)) \to (w -_{G} (k \underset{˙}{\cdot} A) = P \underset{˙}{\cdot} C \leftrightarrow (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) = w)$
73	54 58 62 70 72	syl13anc	$⊢ ((φ \land k \in ℤ) \land w \in W) \to (w -_{G} (k \underset{˙}{\cdot} A) = P \underset{˙}{\cdot} C \leftrightarrow (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) = w)$
74		eqcom	$⊢ P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A) \leftrightarrow w -_{G} (k \underset{˙}{\cdot} A) = P \underset{˙}{\cdot} C$
75		eqcom	$⊢ w = (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \leftrightarrow (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) = w$
76	73 74 75	3bitr4g	$⊢ ((φ \land k \in ℤ) \land w \in W) \to (P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A) \leftrightarrow w = (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A))$
77	76	rexbidva	$⊢ (φ \land k \in ℤ) \to (\exists w \in W P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A) \leftrightarrow \exists w \in W w = (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A))$
78		risset	$⊢ (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W \leftrightarrow \exists w \in W w = (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A)$
79	77 78	bitr4di	$⊢ (φ \land k \in ℤ) \to (\exists w \in W P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A) \leftrightarrow (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)$
80	79	rexbidva	$⊢ φ \to (\exists k \in ℤ \exists w \in W P \underset{˙}{\cdot} C = w -_{G} (k \underset{˙}{\cdot} A) \leftrightarrow \exists k \in ℤ (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)$
81	53 80	mpbid	$⊢ φ \to \exists k \in ℤ (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W$
82	8	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to P pGrp G$
83	9	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to G \in Abel$
84	10	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to B \in Fin$
85	11	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to O (A) = E$
86	12	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to U \in SubGrp (G)$
87	13	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to A \in U$
88	14	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to W \in SubGrp (G)$
89	15	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to S \cap W = \{\underset{˙}{0}\}$
90	16	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to S \underset{˙}{\oplus} W \subseteq U$
91	17	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to \forall w \in SubGrp (G) ((w \subset U \land A \in w) \to \neg S \underset{˙}{\oplus} W \subset w)$
92	18	adantr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to C \in (U ∖ (S \underset{˙}{\oplus} W))$
93		simprl	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to k \in ℤ$
94		simprr	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W$
95		eqid	$⊢ C +_{G} ((\frac{k}{P}) \underset{˙}{\cdot} A) = C +_{G} ((\frac{k}{P}) \underset{˙}{\cdot} A)$
96	1 2 3 4 5 6 7 82 83 84 85 86 87 88 89 90 91 92 19 93 94 95	pgpfac1lem3	$⊢ (φ \land (k \in ℤ \land (P \underset{˙}{\cdot} C) +_{G} (k \underset{˙}{\cdot} A) \in W)) \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$
97	81 96	rexlimddv	$⊢ φ \to \exists t \in SubGrp (G) (S \cap t = \{\underset{˙}{0}\} \land S \underset{˙}{\oplus} t = U)$

Metamath Proof Explorer

Theorem pgpfac1lem4

Proof