# 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}\mathrm{freeLMod}{I}$
frlmbas.n ${⊢}{N}={\mathrm{Base}}_{{R}}$
frlmbas.z
frlmbas.b
Assertion frlmbas ${⊢}\left({R}\in {V}\wedge {I}\in {W}\right)\to {B}={\mathrm{Base}}_{{F}}$

### Proof

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