Metamath Proof Explorer

Theorem frlmpwfi

Description: Formal linear combinations over Z/2Z are equivalent to finite subsets. MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015) (Proof shortened by AV, 14-Jun-2020)

Ref Expression
Hypotheses frlmpwfi.r 
|- R = ( Z/nZ ` 2 )
frlmpwfi.y 
|- Y = ( R freeLMod I )
frlmpwfi.b 
|- B = ( Base ` Y )
Assertion frlmpwfi 
|- ( I e. V -> B ~~ ( ~P I i^i Fin ) )

Proof

Step Hyp Ref Expression
1 frlmpwfi.r 
 |-  R = ( Z/nZ ` 2 )
2 frlmpwfi.y 
 |-  Y = ( R freeLMod I )
3 frlmpwfi.b 
 |-  B = ( Base ` Y )
4 1 fvexi 
 |-  R e. _V
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
7 eqid 
 |-  { x e. ( ( Base ` R ) ^m I ) | x finSupp ( 0g ` R ) } = { x e. ( ( Base ` R ) ^m I ) | x finSupp ( 0g ` R ) }
8 2 5 6 7 frlmbas 
 |-  ( ( R e. _V /\ I e. V ) -> { x e. ( ( Base ` R ) ^m I ) | x finSupp ( 0g ` R ) } = ( Base ` Y ) )
9 4 8 mpan 
 |-  ( I e. V -> { x e. ( ( Base ` R ) ^m I ) | x finSupp ( 0g ` R ) } = ( Base ` Y ) )
10 9 3 eqtr4di 
 |-  ( I e. V -> { x e. ( ( Base ` R ) ^m I ) | x finSupp ( 0g ` R ) } = B )
11 eqid 
 |-  { x e. ( 2o ^m I ) | x finSupp (/) } = { x e. ( 2o ^m I ) | x finSupp (/) }
12 enrefg 
 |-  ( I e. V -> I ~~ I )
13 2nn 
 |-  2 e. NN
14 1 5 znhash 
 |-  ( 2 e. NN -> ( # ` ( Base ` R ) ) = 2 )
15 13 14 ax-mp 
 |-  ( # ` ( Base ` R ) ) = 2
16 hash2 
 |-  ( # ` 2o ) = 2
17 15 16 eqtr4i 
 |-  ( # ` ( Base ` R ) ) = ( # ` 2o )
18 2nn0 
 |-  2 e. NN0
19 15 18 eqeltri 
 |-  ( # ` ( Base ` R ) ) e. NN0
20 fvex 
 |-  ( Base ` R ) e. _V
21 hashclb 
 |-  ( ( Base ` R ) e. _V -> ( ( Base ` R ) e. Fin <-> ( # ` ( Base ` R ) ) e. NN0 ) )
22 20 21 ax-mp 
 |-  ( ( Base ` R ) e. Fin <-> ( # ` ( Base ` R ) ) e. NN0 )
23 19 22 mpbir 
 |-  ( Base ` R ) e. Fin
24 2onn 
 |-  2o e. _om
25 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
26 24 25 ax-mp 
 |-  2o e. Fin
27 hashen 
 |-  ( ( ( Base ` R ) e. Fin /\ 2o e. Fin ) -> ( ( # ` ( Base ` R ) ) = ( # ` 2o ) <-> ( Base ` R ) ~~ 2o ) )
28 23 26 27 mp2an 
 |-  ( ( # ` ( Base ` R ) ) = ( # ` 2o ) <-> ( Base ` R ) ~~ 2o )
29 17 28 mpbi 
 |-  ( Base ` R ) ~~ 2o
30 29 a1i 
 |-  ( I e. V -> ( Base ` R ) ~~ 2o )
31 1 zncrng 
 |-  ( 2 e. NN0 -> R e. CRing )
32 crngring 
 |-  ( R e. CRing -> R e. Ring )
33 18 31 32 mp2b 
 |-  R e. Ring
34 5 6 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
35 33 34 mp1i 
 |-  ( I e. V -> ( 0g ` R ) e. ( Base ` R ) )
36 2on0 
 |-  2o =/= (/)
37 2on 
 |-  2o e. On
38 on0eln0 
 |-  ( 2o e. On -> ( (/) e. 2o <-> 2o =/= (/) ) )
39 37 38 ax-mp 
 |-  ( (/) e. 2o <-> 2o =/= (/) )
40 36 39 mpbir 
 |-  (/) e. 2o
41 40 a1i 
 |-  ( I e. V -> (/) e. 2o )
42 7 11 12 30 35 41 mapfien2 
 |-  ( I e. V -> { x e. ( ( Base ` R ) ^m I ) | x finSupp ( 0g ` R ) } ~~ { x e. ( 2o ^m I ) | x finSupp (/) } )
43 10 42 eqbrtrrd 
 |-  ( I e. V -> B ~~ { x e. ( 2o ^m I ) | x finSupp (/) } )
44 11 pwfi2en 
 |-  ( I e. V -> { x e. ( 2o ^m I ) | x finSupp (/) } ~~ ( ~P I i^i Fin ) )
45 entr 
 |-  ( ( B ~~ { x e. ( 2o ^m I ) | x finSupp (/) } /\ { x e. ( 2o ^m I ) | x finSupp (/) } ~~ ( ~P I i^i Fin ) ) -> B ~~ ( ~P I i^i Fin ) )
46 43 44 45 syl2anc 
 |-  ( I e. V -> B ~~ ( ~P I i^i Fin ) )