pgpfac

Description: Full factorization of a finite abelian p-group, by iterating pgpfac1 . There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

	Ref	Expression
Hypotheses	pgpfac.b	$⊢ B = {Base}_{G}$
	pgpfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
	pgpfac.g	$⊢ φ \to G \in Abel$
	pgpfac.p	$⊢ φ \to P pGrp G$
	pgpfac.f	$⊢ φ \to B \in Fin$
Assertion	pgpfac	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$

Proof

Step	Hyp	Ref	Expression
1		pgpfac.b	$⊢ B = {Base}_{G}$
2		pgpfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
3		pgpfac.g	$⊢ φ \to G \in Abel$
4		pgpfac.p	$⊢ φ \to P pGrp G$
5		pgpfac.f	$⊢ φ \to B \in Fin$
6		ablgrp	$⊢ G \in Abel \to G \in Grp$
7	1	subgid	$⊢ G \in Grp \to B \in SubGrp (G)$
8	3 6 7	3syl	$⊢ φ \to B \in SubGrp (G)$
9		eleq1	$⊢ t = u \to (t \in SubGrp (G) \leftrightarrow u \in SubGrp (G))$
10		eqeq2	$⊢ t = u \to (G DProd s = t \leftrightarrow G DProd s = u)$
11	10	anbi2d	$⊢ t = u \to ((G dom DProd s \land G DProd s = t) \leftrightarrow (G dom DProd s \land G DProd s = u))$
12	11	rexbidv	$⊢ t = u \to (\exists s \in Word C (G dom DProd s \land G DProd s = t) \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = u))$
13	9 12	imbi12d	$⊢ t = u \to ((t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \leftrightarrow (u \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = u)))$
14	13	imbi2d	$⊢ t = u \to ((φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t))) \leftrightarrow (φ \to (u \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = u))))$
15		eleq1	$⊢ t = B \to (t \in SubGrp (G) \leftrightarrow B \in SubGrp (G))$
16		eqeq2	$⊢ t = B \to (G DProd s = t \leftrightarrow G DProd s = B)$
17	16	anbi2d	$⊢ t = B \to ((G dom DProd s \land G DProd s = t) \leftrightarrow (G dom DProd s \land G DProd s = B))$
18	17	rexbidv	$⊢ t = B \to (\exists s \in Word C (G dom DProd s \land G DProd s = t) \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = B))$
19	15 18	imbi12d	$⊢ t = B \to ((t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \leftrightarrow (B \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = B)))$
20	19	imbi2d	$⊢ t = B \to ((φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t))) \leftrightarrow (φ \to (B \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = B))))$
21		bi2.04	$⊢ (t \subset u \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t))) \leftrightarrow (t \in SubGrp (G) \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))$
22	21	imbi2i	$⊢ (φ \to (t \subset u \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \leftrightarrow (φ \to (t \in SubGrp (G) \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))))$
23		bi2.04	$⊢ (t \subset u \to (φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \leftrightarrow (φ \to (t \subset u \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t))))$
24		bi2.04	$⊢ (t \in SubGrp (G) \to (φ \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \leftrightarrow (φ \to (t \in SubGrp (G) \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))))$
25	22 23 24	3bitr4i	$⊢ (t \subset u \to (φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \leftrightarrow (t \in SubGrp (G) \to (φ \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))))$
26	25	albii	$⊢ \forall t (t \subset u \to (φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \leftrightarrow \forall t (t \in SubGrp (G) \to (φ \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))))$
27		df-ral	$⊢ \forall t \in SubGrp (G) (φ \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))) \leftrightarrow \forall t (t \in SubGrp (G) \to (φ \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))))$
28		r19.21v	$⊢ \forall t \in SubGrp (G) (φ \to (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))) \leftrightarrow (φ \to \forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))$
29	26 27 28	3bitr2i	$⊢ \forall t (t \subset u \to (φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \leftrightarrow (φ \to \forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))$
30	3	adantr	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to G \in Abel$
31	4	adantr	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to P pGrp G$
32	5	adantr	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to B \in Fin$
33		simprr	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to u \in SubGrp (G)$
34		simprl	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to \forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))$
35		psseq1	$⊢ t = x \to (t \subset u \leftrightarrow x \subset u)$
36		eqeq2	$⊢ t = x \to (G DProd s = t \leftrightarrow G DProd s = x)$
37	36	anbi2d	$⊢ t = x \to ((G dom DProd s \land G DProd s = t) \leftrightarrow (G dom DProd s \land G DProd s = x))$
38	37	rexbidv	$⊢ t = x \to (\exists s \in Word C (G dom DProd s \land G DProd s = t) \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = x))$
39	35 38	imbi12d	$⊢ t = x \to ((t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \leftrightarrow (x \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = x)))$
40	39	cbvralvw	$⊢ \forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \leftrightarrow \forall x \in SubGrp (G) (x \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = x))$
41	34 40	sylib	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to \forall x \in SubGrp (G) (x \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = x))$
42	1 2 30 31 32 33 41	pgpfaclem3	$⊢ (φ \land (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \land u \in SubGrp (G))) \to \exists s \in Word C (G dom DProd s \land G DProd s = u)$
43	42	exp32	$⊢ φ \to (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \to (u \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = u)))$
44	43	a1i	$⊢ u \in Fin \to (φ \to (\forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t)) \to (u \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = u))))$
45	44	a2d	$⊢ u \in Fin \to ((φ \to \forall t \in SubGrp (G) (t \subset u \to \exists s \in Word C (G dom DProd s \land G DProd s = t))) \to (φ \to (u \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = u))))$
46	29 45	syl5bi	$⊢ u \in Fin \to (\forall t (t \subset u \to (φ \to (t \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = t)))) \to (φ \to (u \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = u))))$
47	14 20 46	findcard3	$⊢ B \in Fin \to (φ \to (B \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = B)))$
48	5 47	mpcom	$⊢ φ \to (B \in SubGrp (G) \to \exists s \in Word C (G dom DProd s \land G DProd s = B))$
49	8 48	mpd	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$

Metamath Proof Explorer

Theorem pgpfac

Proof