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