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 ) )