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 e. dom card /\ S =/= (/) ) -> S e. ( Base " Abel ) )

Proof

Step Hyp Ref Expression
1 hashcl 
 |-  ( S e. Fin -> ( # ` S ) e. NN0 )
2 1 adantl 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( # ` S ) e. NN0 )
3 eqid 
 |-  ( Z/nZ ` ( # ` S ) ) = ( Z/nZ ` ( # ` S ) )
4 3 zncrng 
 |-  ( ( # ` S ) e. NN0 -> ( Z/nZ ` ( # ` S ) ) e. CRing )
5 crngring 
 |-  ( ( Z/nZ ` ( # ` S ) ) e. CRing -> ( Z/nZ ` ( # ` S ) ) e. Ring )
6 ringabl 
 |-  ( ( Z/nZ ` ( # ` S ) ) e. Ring -> ( Z/nZ ` ( # ` S ) ) e. Abel )
7 2 4 5 6 4syl 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( Z/nZ ` ( # ` S ) ) e. Abel )
8 hashnncl 
 |-  ( S e. Fin -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
9 8 biimparc 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( # ` S ) e. NN )
10 eqid 
 |-  ( Base ` ( Z/nZ ` ( # ` S ) ) ) = ( Base ` ( Z/nZ ` ( # ` S ) ) )
11 3 10 znhash 
 |-  ( ( # ` S ) e. NN -> ( # ` ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) = ( # ` S ) )
12 9 11 syl 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( # ` ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) = ( # ` S ) )
13 12 eqcomd 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( # ` S ) = ( # ` ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) )
14 simpr 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> S e. Fin )
15 3 10 znfi 
 |-  ( ( # ` S ) e. NN -> ( Base ` ( Z/nZ ` ( # ` S ) ) ) e. Fin )
16 9 15 syl 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( Base ` ( Z/nZ ` ( # ` S ) ) ) e. Fin )
17 hashen 
 |-  ( ( S e. Fin /\ ( Base ` ( Z/nZ ` ( # ` S ) ) ) e. Fin ) -> ( ( # ` S ) = ( # ` ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) <-> S ~~ ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) )
18 14 16 17 syl2anc 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> ( ( # ` S ) = ( # ` ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) <-> S ~~ ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) )
19 13 18 mpbid 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> S ~~ ( Base ` ( Z/nZ ` ( # ` S ) ) ) )
20 10 isnumbasgrplem1 
 |-  ( ( ( Z/nZ ` ( # ` S ) ) e. Abel /\ S ~~ ( Base ` ( Z/nZ ` ( # ` S ) ) ) ) -> S e. ( Base " Abel ) )
21 7 19 20 syl2anc 
 |-  ( ( S =/= (/) /\ S e. Fin ) -> S e. ( Base " Abel ) )
22 21 adantll 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ S e. Fin ) -> S e. ( Base " Abel ) )
23 2nn0 
 |-  2 e. NN0
24 eqid 
 |-  ( Z/nZ ` 2 ) = ( Z/nZ ` 2 )
25 24 zncrng 
 |-  ( 2 e. NN0 -> ( Z/nZ ` 2 ) e. CRing )
26 crngring 
 |-  ( ( Z/nZ ` 2 ) e. CRing -> ( Z/nZ ` 2 ) e. Ring )
27 23 25 26 mp2b 
 |-  ( Z/nZ ` 2 ) e. Ring
28 eqid 
 |-  ( ( Z/nZ ` 2 ) freeLMod S ) = ( ( Z/nZ ` 2 ) freeLMod S )
29 28 frlmlmod 
 |-  ( ( ( Z/nZ ` 2 ) e. Ring /\ S e. dom card ) -> ( ( Z/nZ ` 2 ) freeLMod S ) e. LMod )
30 27 29 mpan 
 |-  ( S e. dom card -> ( ( Z/nZ ` 2 ) freeLMod S ) e. LMod )
31 lmodabl 
 |-  ( ( ( Z/nZ ` 2 ) freeLMod S ) e. LMod -> ( ( Z/nZ ` 2 ) freeLMod S ) e. Abel )
32 30 31 syl 
 |-  ( S e. dom card -> ( ( Z/nZ ` 2 ) freeLMod S ) e. Abel )
33 32 ad2antrr 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> ( ( Z/nZ ` 2 ) freeLMod S ) e. Abel )
34 eqid 
 |-  ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) = ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) )
35 24 28 34 frlmpwfi 
 |-  ( S e. dom card -> ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) ~~ ( ~P S i^i Fin ) )
36 35 ad2antrr 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) ~~ ( ~P S i^i Fin ) )
37 simpll 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> S e. dom card )
38 numinfctb 
 |-  ( ( S e. dom card /\ -. S e. Fin ) -> _om ~<_ S )
39 38 adantlr 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> _om ~<_ S )
40 infpwfien 
 |-  ( ( S e. dom card /\ _om ~<_ S ) -> ( ~P S i^i Fin ) ~~ S )
41 37 39 40 syl2anc 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> ( ~P S i^i Fin ) ~~ S )
42 entr 
 |-  ( ( ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) ~~ ( ~P S i^i Fin ) /\ ( ~P S i^i Fin ) ~~ S ) -> ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) ~~ S )
43 36 41 42 syl2anc 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) ~~ S )
44 43 ensymd 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> S ~~ ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) )
45 34 isnumbasgrplem1 
 |-  ( ( ( ( Z/nZ ` 2 ) freeLMod S ) e. Abel /\ S ~~ ( Base ` ( ( Z/nZ ` 2 ) freeLMod S ) ) ) -> S e. ( Base " Abel ) )
46 33 44 45 syl2anc 
 |-  ( ( ( S e. dom card /\ S =/= (/) ) /\ -. S e. Fin ) -> S e. ( Base " Abel ) )
47 22 46 pm2.61dan 
 |-  ( ( S e. dom card /\ S =/= (/) ) -> S e. ( Base " Abel ) )