Metamath Proof Explorer

Theorem ablfac

Description: The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		ablfac.b	$⊢ B = {Base}_{G}$
2		ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
3		ablfac.1	$⊢ φ \to G \in Abel$
4		ablfac.2	$⊢ φ \to B \in Fin$
5		ablgrp	$⊢ G \in Abel \to G \in Grp$
6	1	subgid	$⊢ G \in Grp \to B \in SubGrp (G)$
7		eqid	$⊢ od (G) = od (G)$
8		eqid	$⊢ \{w \in ℙ \| w ∥ \|B\|\} = \{w \in ℙ \| w ∥ \|B\|\}$
9		eqid	$⊢ (p \in \{w \in ℙ \| w ∥ \|B\|\} ⟼ \{x \in B \| od (G) (x) ∥ p^{p pCnt \|B\|}\}) = (p \in \{w \in ℙ \| w ∥ \|B\|\} ⟼ \{x \in B \| od (G) (x) ∥ p^{p pCnt \|B\|}\})$
10		eqid	$⊢ (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\}) = (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\})$
11	1 2 3 4 7 8 9 10	ablfaclem1	$⊢ B \in SubGrp (G) \to (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\}) (B) = \{s \in Word C \| (G dom DProd s \land G DProd s = B)\}$
12	3 5 6 11	4syl	$⊢ φ \to (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\}) (B) = \{s \in Word C \| (G dom DProd s \land G DProd s = B)\}$
13	1 2 3 4 7 8 9 10	ablfaclem3	$⊢ φ \to (g \in SubGrp (G) ⟼ \{s \in Word C \| (G dom DProd s \land G DProd s = g)\}) (B) \neq \emptyset$
14	12 13	eqnetrrd	$⊢ φ \to \{s \in Word C \| (G dom DProd s \land G DProd s = B)\} \neq \emptyset$
15		rabn0	$⊢ \{s \in Word C \| (G dom DProd s \land G DProd s = B)\} \neq \emptyset \leftrightarrow \exists s \in Word C (G dom DProd s \land G DProd s = B)$
16	14 15	sylib	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$