Metamath Proof Explorer

Theorem frlmbas

Description: Base set of the free module. (Contributed by Stefan O'Rear, 1-Feb-2015) (Revised by AV, 23-Jun-2019)

Ref Expression
Hypotheses frlmval.f 
|- F = ( R freeLMod I )
frlmbas.n 
|- N = ( Base ` R )
frlmbas.z 
|- .0. = ( 0g ` R )
frlmbas.b 
|- B = { k e. ( N ^m I ) | k finSupp .0. }
Assertion frlmbas 
|- ( ( R e. V /\ I e. W ) -> B = ( Base ` F ) )

Proof

Step Hyp Ref Expression
1 frlmval.f 
 |-  F = ( R freeLMod I )
2 frlmbas.n 
 |-  N = ( Base ` R )
3 frlmbas.z 
 |-  .0. = ( 0g ` R )
4 frlmbas.b 
 |-  B = { k e. ( N ^m I ) | k finSupp .0. }
5 fvex 
 |-  ( ringLMod ` R ) e. _V
6 fnconstg 
 |-  ( ( ringLMod ` R ) e. _V -> ( I X. { ( ringLMod ` R ) } ) Fn I )
7 5 6 ax-mp 
 |-  ( I X. { ( ringLMod ` R ) } ) Fn I
8 eqid 
 |-  ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) )
9 eqid 
 |-  { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } = { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin }
10 8 9 dsmmbas2 
 |-  ( ( ( I X. { ( ringLMod ` R ) } ) Fn I /\ I e. W ) -> { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
11 7 10 mpan 
 |-  ( I e. W -> { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
12 11 adantl 
 |-  ( ( R e. V /\ I e. W ) -> { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
13 fvco2 
 |-  ( ( ( I X. { ( ringLMod ` R ) } ) Fn I /\ x e. I ) -> ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) = ( 0g ` ( ( I X. { ( ringLMod ` R ) } ) ` x ) ) )
14 7 13 mpan 
 |-  ( x e. I -> ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) = ( 0g ` ( ( I X. { ( ringLMod ` R ) } ) ` x ) ) )
15 14 adantl 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) /\ x e. I ) -> ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) = ( 0g ` ( ( I X. { ( ringLMod ` R ) } ) ` x ) ) )
16 5 fvconst2 
 |-  ( x e. I -> ( ( I X. { ( ringLMod ` R ) } ) ` x ) = ( ringLMod ` R ) )
17 16 adantl 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) /\ x e. I ) -> ( ( I X. { ( ringLMod ` R ) } ) ` x ) = ( ringLMod ` R ) )
18 17 fveq2d 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) /\ x e. I ) -> ( 0g ` ( ( I X. { ( ringLMod ` R ) } ) ` x ) ) = ( 0g ` ( ringLMod ` R ) ) )
19 rlm0 
 |-  ( 0g ` R ) = ( 0g ` ( ringLMod ` R ) )
20 3 19 eqtri 
 |-  .0. = ( 0g ` ( ringLMod ` R ) )
21 18 20 eqtr4di 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) /\ x e. I ) -> ( 0g ` ( ( I X. { ( ringLMod ` R ) } ) ` x ) ) = .0. )
22 15 21 eqtrd 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) /\ x e. I ) -> ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) = .0. )
23 22 neeq2d 
 |-  ( ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) /\ x e. I ) -> ( ( k ` x ) =/= ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) <-> ( k ` x ) =/= .0. ) )
24 23 rabbidva 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> { x e. I | ( k ` x ) =/= ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) } = { x e. I | ( k ` x ) =/= .0. } )
25 elmapfn 
 |-  ( k e. ( N ^m I ) -> k Fn I )
26 25 adantl 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> k Fn I )
27 fn0g 
 |-  0g Fn _V
28 ssv 
 |-  ran ( I X. { ( ringLMod ` R ) } ) C_ _V
29 fnco 
 |-  ( ( 0g Fn _V /\ ( I X. { ( ringLMod ` R ) } ) Fn I /\ ran ( I X. { ( ringLMod ` R ) } ) C_ _V ) -> ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) Fn I )
30 27 7 28 29 mp3an 
 |-  ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) Fn I
31 fndmdif 
 |-  ( ( k Fn I /\ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) Fn I ) -> dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) = { x e. I | ( k ` x ) =/= ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) } )
32 26 30 31 sylancl 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) = { x e. I | ( k ` x ) =/= ( ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ` x ) } )
33 simplr 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> I e. W )
34 3 fvexi 
 |-  .0. e. _V
35 34 a1i 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> .0. e. _V )
36 suppvalfn 
 |-  ( ( k Fn I /\ I e. W /\ .0. e. _V ) -> ( k supp .0. ) = { x e. I | ( k ` x ) =/= .0. } )
37 26 33 35 36 syl3anc 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> ( k supp .0. ) = { x e. I | ( k ` x ) =/= .0. } )
38 24 32 37 3eqtr4d 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) = ( k supp .0. ) )
39 38 eleq1d 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> ( dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin <-> ( k supp .0. ) e. Fin ) )
40 elmapfun 
 |-  ( k e. ( N ^m I ) -> Fun k )
41 id 
 |-  ( k e. ( N ^m I ) -> k e. ( N ^m I ) )
42 34 a1i 
 |-  ( k e. ( N ^m I ) -> .0. e. _V )
43 40 41 42 3jca 
 |-  ( k e. ( N ^m I ) -> ( Fun k /\ k e. ( N ^m I ) /\ .0. e. _V ) )
44 43 adantl 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> ( Fun k /\ k e. ( N ^m I ) /\ .0. e. _V ) )
45 funisfsupp 
 |-  ( ( Fun k /\ k e. ( N ^m I ) /\ .0. e. _V ) -> ( k finSupp .0. <-> ( k supp .0. ) e. Fin ) )
46 44 45 syl 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> ( k finSupp .0. <-> ( k supp .0. ) e. Fin ) )
47 39 46 bitr4d 
 |-  ( ( ( R e. V /\ I e. W ) /\ k e. ( N ^m I ) ) -> ( dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin <-> k finSupp .0. ) )
48 47 rabbidva 
 |-  ( ( R e. V /\ I e. W ) -> { k e. ( N ^m I ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } = { k e. ( N ^m I ) | k finSupp .0. } )
49 eqid 
 |-  ( ( ringLMod ` R ) ^s I ) = ( ( ringLMod ` R ) ^s I )
50 rlmbas 
 |-  ( Base ` R ) = ( Base ` ( ringLMod ` R ) )
51 2 50 eqtri 
 |-  N = ( Base ` ( ringLMod ` R ) )
52 49 51 pwsbas 
 |-  ( ( ( ringLMod ` R ) e. _V /\ I e. W ) -> ( N ^m I ) = ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
53 5 52 mpan 
 |-  ( I e. W -> ( N ^m I ) = ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
54 53 adantl 
 |-  ( ( R e. V /\ I e. W ) -> ( N ^m I ) = ( Base ` ( ( ringLMod ` R ) ^s I ) ) )
55 eqid 
 |-  ( Scalar ` ( ringLMod ` R ) ) = ( Scalar ` ( ringLMod ` R ) )
56 49 55 pwsval 
 |-  ( ( ( ringLMod ` R ) e. _V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
57 5 56 mpan 
 |-  ( I e. W -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
58 57 adantl 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
59 rlmsca 
 |-  ( R e. V -> R = ( Scalar ` ( ringLMod ` R ) ) )
60 59 adantr 
 |-  ( ( R e. V /\ I e. W ) -> R = ( Scalar ` ( ringLMod ` R ) ) )
61 60 oveq1d 
 |-  ( ( R e. V /\ I e. W ) -> ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) = ( ( Scalar ` ( ringLMod ` R ) ) Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
62 58 61 eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> ( ( ringLMod ` R ) ^s I ) = ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) )
63 62 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` ( ( ringLMod ` R ) ^s I ) ) = ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) )
64 54 63 eqtrd 
 |-  ( ( R e. V /\ I e. W ) -> ( N ^m I ) = ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) )
65 64 rabeqdv 
 |-  ( ( R e. V /\ I e. W ) -> { k e. ( N ^m I ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } = { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } )
66 48 65 eqtr3d 
 |-  ( ( R e. V /\ I e. W ) -> { k e. ( N ^m I ) | k finSupp .0. } = { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } )
67 4 66 syl5eq 
 |-  ( ( R e. V /\ I e. W ) -> B = { k e. ( Base ` ( R Xs_ ( I X. { ( ringLMod ` R ) } ) ) ) | dom ( k \ ( 0g o. ( I X. { ( ringLMod ` R ) } ) ) ) e. Fin } )
68 1 frlmval 
 |-  ( ( R e. V /\ I e. W ) -> F = ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) )
69 68 fveq2d 
 |-  ( ( R e. V /\ I e. W ) -> ( Base ` F ) = ( Base ` ( R (+)m ( I X. { ( ringLMod ` R ) } ) ) ) )
70 12 67 69 3eqtr4d 
 |-  ( ( R e. V /\ I e. W ) -> B = ( Base ` F ) )