Metamath Proof Explorer

Theorem 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 ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) → 𝑆 ∈ ( Base “ Abel ) )

Proof

Step Hyp Ref Expression
1 hashcl ⊢ ( 𝑆 ∈ Fin → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
2 1 adantl ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
3 eqid ⊢ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) = ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) )
4 3 zncrng ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ0 → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ CRing )
5 crngring ⊢ ( ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ CRing → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Ring )
6 ringabl ⊢ ( ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Ring → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Abel )
7 2 4 5 6 4syl ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Abel )
8 hashnncl ⊢ ( 𝑆 ∈ Fin → ( ( ♯ ‘ 𝑆 ) ∈ ℕ ↔ 𝑆 ≠ ∅ ) )
9 8 biimparc ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ 𝑆 ) ∈ ℕ )
10 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) = ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) )
11 3 10 znhash ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ → ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) = ( ♯ ‘ 𝑆 ) )
12 9 11 syl ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) = ( ♯ ‘ 𝑆 ) )
13 12 eqcomd ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) )
14 simpr ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ Fin )
15 3 10 znfi ⊢ ( ( ♯ ‘ 𝑆 ) ∈ ℕ → ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ∈ Fin )
16 9 15 syl ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ∈ Fin )
17 hashen ⊢ ( ( 𝑆 ∈ Fin ∧ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ↔ 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) )
18 14 16 17 syl2anc ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → ( ( ♯ ‘ 𝑆 ) = ( ♯ ‘ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) ↔ 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) )
19 13 18 mpbid ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) )
20 10 isnumbasgrplem1 ⊢ ( ( ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ∈ Abel ∧ 𝑆 ≈ ( Base ‘ ( ℤ/nℤ ‘ ( ♯ ‘ 𝑆 ) ) ) ) → 𝑆 ∈ ( Base “ Abel ) )
21 7 19 20 syl2anc ⊢ ( ( 𝑆 ≠ ∅ ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ ( Base “ Abel ) )
22 21 adantll ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ 𝑆 ∈ Fin ) → 𝑆 ∈ ( Base “ Abel ) )
23 2nn0 ⊢ 2 ∈ ℕ0
24 eqid ⊢ ( ℤ/nℤ ‘ 2 ) = ( ℤ/nℤ ‘ 2 )
25 24 zncrng ⊢ ( 2 ∈ ℕ0 → ( ℤ/nℤ ‘ 2 ) ∈ CRing )
26 crngring ⊢ ( ( ℤ/nℤ ‘ 2 ) ∈ CRing → ( ℤ/nℤ ‘ 2 ) ∈ Ring )
27 23 25 26 mp2b ⊢ ( ℤ/nℤ ‘ 2 ) ∈ Ring
28 eqid ⊢ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) = ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 )
29 28 frlmlmod ⊢ ( ( ( ℤ/nℤ ‘ 2 ) ∈ Ring ∧ 𝑆 ∈ dom card ) → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ LMod )
30 27 29 mpan ⊢ ( 𝑆 ∈ dom card → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ LMod )
31 lmodabl ⊢ ( ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ LMod → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel )
32 30 31 syl ⊢ ( 𝑆 ∈ dom card → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel )
33 32 ad2antrr ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel )
34 eqid ⊢ ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) = ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) )
35 24 28 34 frlmpwfi ⊢ ( 𝑆 ∈ dom card → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ ( 𝒫 𝑆 ∩ Fin ) )
36 35 ad2antrr ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ ( 𝒫 𝑆 ∩ Fin ) )
37 simpll ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ∈ dom card )
38 numinfctb ⊢ ( ( 𝑆 ∈ dom card ∧ ¬ 𝑆 ∈ Fin ) → ω ≼ 𝑆 )
39 38 adantlr ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ω ≼ 𝑆 )
40 infpwfien ⊢ ( ( 𝑆 ∈ dom card ∧ ω ≼ 𝑆 ) → ( 𝒫 𝑆 ∩ Fin ) ≈ 𝑆 )
41 37 39 40 syl2anc ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( 𝒫 𝑆 ∩ Fin ) ≈ 𝑆 )
42 entr ⊢ ( ( ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ ( 𝒫 𝑆 ∩ Fin ) ∧ ( 𝒫 𝑆 ∩ Fin ) ≈ 𝑆 ) → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ 𝑆 )
43 36 41 42 syl2anc ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ≈ 𝑆 )
44 43 ensymd ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ≈ ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) )
45 34 isnumbasgrplem1 ⊢ ( ( ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ∈ Abel ∧ 𝑆 ≈ ( Base ‘ ( ( ℤ/nℤ ‘ 2 ) freeLMod 𝑆 ) ) ) → 𝑆 ∈ ( Base “ Abel ) )
46 33 44 45 syl2anc ⊢ ( ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) ∧ ¬ 𝑆 ∈ Fin ) → 𝑆 ∈ ( Base “ Abel ) )
47 22 46 pm2.61dan ⊢ ( ( 𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ) → 𝑆 ∈ ( Base “ Abel ) )