isnumbasgrplem3

Description: Every nonempty numerable set can be given the structure of an Abelian group, either a finite cyclic group or a vector space over Z/2Z. (Contributed by Stefan O'Rear, 10-Jul-2015)

		Ref	Expression
	Assertion	isnumbasgrplem3	$⊢ (S \in dom card \land S \neq \emptyset) \to S \in Base [Abel]$

Proof

Step	Hyp	Ref	Expression
1		hashcl	$⊢ S \in Fin \to \|S\| \in ℕ_{0}$
2	1	adantl	$⊢ (S \neq \emptyset \land S \in Fin) \to \|S\| \in ℕ_{0}$
3		eqid	$⊢ ℤ / \|S\| ℤ = ℤ / \|S\| ℤ$
4	3	zncrng	$⊢ \|S\| \in ℕ_{0} \to ℤ / \|S\| ℤ \in CRing$
5		crngring	$⊢ ℤ / \|S\| ℤ \in CRing \to ℤ / \|S\| ℤ \in Ring$
6		ringabl	$⊢ ℤ / \|S\| ℤ \in Ring \to ℤ / \|S\| ℤ \in Abel$
7	2 4 5 6	4syl	$⊢ (S \neq \emptyset \land S \in Fin) \to ℤ / \|S\| ℤ \in Abel$
8		hashnncl	$⊢ S \in Fin \to (\|S\| \in ℕ \leftrightarrow S \neq \emptyset)$
9	8	biimparc	$⊢ (S \neq \emptyset \land S \in Fin) \to \|S\| \in ℕ$
10		eqid	$⊢ {Base}_{ℤ / \|S\| ℤ} = {Base}_{ℤ / \|S\| ℤ}$
11	3 10	znhash	$⊢ \|S\| \in ℕ \to \|{Base}_{ℤ / \|S\| ℤ}\| = \|S\|$
12	9 11	syl	$⊢ (S \neq \emptyset \land S \in Fin) \to \|{Base}_{ℤ / \|S\| ℤ}\| = \|S\|$
13	12	eqcomd	$⊢ (S \neq \emptyset \land S \in Fin) \to \|S\| = \|{Base}_{ℤ / \|S\| ℤ}\|$
14		simpr	$⊢ (S \neq \emptyset \land S \in Fin) \to S \in Fin$
15	3 10	znfi	$⊢ \|S\| \in ℕ \to {Base}_{ℤ / \|S\| ℤ} \in Fin$
16	9 15	syl	$⊢ (S \neq \emptyset \land S \in Fin) \to {Base}_{ℤ / \|S\| ℤ} \in Fin$
17		hashen	$⊢ (S \in Fin \land {Base}_{ℤ / \|S\| ℤ} \in Fin) \to (\|S\| = \|{Base}_{ℤ / \|S\| ℤ}\| \leftrightarrow S \approx {Base}_{ℤ / \|S\| ℤ})$
18	14 16 17	syl2anc	$⊢ (S \neq \emptyset \land S \in Fin) \to (\|S\| = \|{Base}_{ℤ / \|S\| ℤ}\| \leftrightarrow S \approx {Base}_{ℤ / \|S\| ℤ})$
19	13 18	mpbid	$⊢ (S \neq \emptyset \land S \in Fin) \to S \approx {Base}_{ℤ / \|S\| ℤ}$
20	10	isnumbasgrplem1	$⊢ (ℤ / \|S\| ℤ \in Abel \land S \approx {Base}_{ℤ / \|S\| ℤ}) \to S \in Base [Abel]$
21	7 19 20	syl2anc	$⊢ (S \neq \emptyset \land S \in Fin) \to S \in Base [Abel]$
22	21	adantll	$⊢ ((S \in dom card \land S \neq \emptyset) \land S \in Fin) \to S \in Base [Abel]$
23		2nn0	$⊢ 2 \in ℕ_{0}$
24		eqid	$⊢ ℤ / 2 ℤ = ℤ / 2 ℤ$
25	24	zncrng	$⊢ 2 \in ℕ_{0} \to ℤ / 2 ℤ \in CRing$
26		crngring	$⊢ ℤ / 2 ℤ \in CRing \to ℤ / 2 ℤ \in Ring$
27	23 25 26	mp2b	$⊢ ℤ / 2 ℤ \in Ring$
28		eqid	$⊢ ℤ / 2 ℤ freeLMod S = ℤ / 2 ℤ freeLMod S$
29	28	frlmlmod	$⊢ (ℤ / 2 ℤ \in Ring \land S \in dom card) \to ℤ / 2 ℤ freeLMod S \in LMod$
30	27 29	mpan	$⊢ S \in dom card \to ℤ / 2 ℤ freeLMod S \in LMod$
31		lmodabl	$⊢ ℤ / 2 ℤ freeLMod S \in LMod \to ℤ / 2 ℤ freeLMod S \in Abel$
32	30 31	syl	$⊢ S \in dom card \to ℤ / 2 ℤ freeLMod S \in Abel$
33	32	ad2antrr	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to ℤ / 2 ℤ freeLMod S \in Abel$
34		eqid	$⊢ {Base}_{(ℤ / 2 ℤ freeLMod S)} = {Base}_{(ℤ / 2 ℤ freeLMod S)}$
35	24 28 34	frlmpwfi	$⊢ S \in dom card \to {Base}_{(ℤ / 2 ℤ freeLMod S)} \approx (𝒫 S \cap Fin)$
36	35	ad2antrr	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to {Base}_{(ℤ / 2 ℤ freeLMod S)} \approx (𝒫 S \cap Fin)$
37		simpll	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to S \in dom card$
38		numinfctb	$⊢ (S \in dom card \land \neg S \in Fin) \to ω ≼ S$
39	38	adantlr	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to ω ≼ S$
40		infpwfien	$⊢ (S \in dom card \land ω ≼ S) \to (𝒫 S \cap Fin) \approx S$
41	37 39 40	syl2anc	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to (𝒫 S \cap Fin) \approx S$
42		entr	$⊢ ({Base}_{(ℤ / 2 ℤ freeLMod S)} \approx (𝒫 S \cap Fin) \land (𝒫 S \cap Fin) \approx S) \to {Base}_{(ℤ / 2 ℤ freeLMod S)} \approx S$
43	36 41 42	syl2anc	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to {Base}_{(ℤ / 2 ℤ freeLMod S)} \approx S$
44	43	ensymd	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to S \approx {Base}_{(ℤ / 2 ℤ freeLMod S)}$
45	34	isnumbasgrplem1	$⊢ (ℤ / 2 ℤ freeLMod S \in Abel \land S \approx {Base}_{(ℤ / 2 ℤ freeLMod S)}) \to S \in Base [Abel]$
46	33 44 45	syl2anc	$⊢ ((S \in dom card \land S \neq \emptyset) \land \neg S \in Fin) \to S \in Base [Abel]$
47	22 46	pm2.61dan	$⊢ (S \in dom card \land S \neq \emptyset) \to S \in Base [Abel]$

Metamath Proof Explorer

Theorem isnumbasgrplem3

Proof