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 S dom card S S Base Abel

Proof

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