# Metamath Proof Explorer

## Theorem uvcff

Description: Domain and range of the unit vector generator; ring condition required to be sure 1 and 0 are actually in the ring. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

Ref Expression
Hypotheses uvcff.u ${⊢}{U}={R}\mathrm{unitVec}{I}$
uvcff.y ${⊢}{Y}={R}\mathrm{freeLMod}{I}$
uvcff.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
Assertion uvcff ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {U}:{I}⟶{B}$

### Proof

Step Hyp Ref Expression
1 uvcff.u ${⊢}{U}={R}\mathrm{unitVec}{I}$
2 uvcff.y ${⊢}{Y}={R}\mathrm{freeLMod}{I}$
3 uvcff.b ${⊢}{B}={\mathrm{Base}}_{{Y}}$
4 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
5 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
6 1 4 5 uvcfval ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {U}=\left({i}\in {I}⟼\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
8 7 4 ringidcl ${⊢}{R}\in \mathrm{Ring}\to {1}_{{R}}\in {\mathrm{Base}}_{{R}}$
9 7 5 ring0cl ${⊢}{R}\in \mathrm{Ring}\to {0}_{{R}}\in {\mathrm{Base}}_{{R}}$
10 8 9 ifcld ${⊢}{R}\in \mathrm{Ring}\to if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
11 10 ad3antrrr ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\wedge {j}\in {I}\right)\to if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\in {\mathrm{Base}}_{{R}}$
12 11 fmpttd ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right):{I}⟶{\mathrm{Base}}_{{R}}$
13 fvex ${⊢}{\mathrm{Base}}_{{R}}\in \mathrm{V}$
14 elmapg ${⊢}\left({\mathrm{Base}}_{{R}}\in \mathrm{V}\wedge {I}\in {W}\right)\to \left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)↔\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right):{I}⟶{\mathrm{Base}}_{{R}}\right)$
15 13 14 mpan ${⊢}{I}\in {W}\to \left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)↔\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right):{I}⟶{\mathrm{Base}}_{{R}}\right)$
16 15 ad2antlr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)↔\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right):{I}⟶{\mathrm{Base}}_{{R}}\right)$
17 12 16 mpbird ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)$
18 mptexg ${⊢}{I}\in {W}\to \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \mathrm{V}$
19 18 ad2antlr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \mathrm{V}$
20 funmpt ${⊢}\mathrm{Fun}\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)$
21 20 a1i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \mathrm{Fun}\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)$
22 fvex ${⊢}{0}_{{R}}\in \mathrm{V}$
23 22 a1i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to {0}_{{R}}\in \mathrm{V}$
24 snfi ${⊢}\left\{{i}\right\}\in \mathrm{Fin}$
25 24 a1i ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left\{{i}\right\}\in \mathrm{Fin}$
26 eldifsni ${⊢}{j}\in \left({I}\setminus \left\{{i}\right\}\right)\to {j}\ne {i}$
27 26 adantl ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\wedge {j}\in \left({I}\setminus \left\{{i}\right\}\right)\right)\to {j}\ne {i}$
28 27 neneqd ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\wedge {j}\in \left({I}\setminus \left\{{i}\right\}\right)\right)\to ¬{j}={i}$
29 28 iffalsed ${⊢}\left(\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\wedge {j}\in \left({I}\setminus \left\{{i}\right\}\right)\right)\to if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)={0}_{{R}}$
30 simplr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to {I}\in {W}$
31 29 30 suppss2 ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\mathrm{supp}{0}_{{R}}\subseteq \left\{{i}\right\}$
32 suppssfifsupp ${⊢}\left(\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \mathrm{V}\wedge \mathrm{Fun}\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\wedge {0}_{{R}}\in \mathrm{V}\right)\wedge \left(\left\{{i}\right\}\in \mathrm{Fin}\wedge \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\mathrm{supp}{0}_{{R}}\subseteq \left\{{i}\right\}\right)\right)\to {finSupp}_{{0}_{{R}}}\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\right)$
33 19 21 23 25 31 32 syl32anc ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to {finSupp}_{{0}_{{R}}}\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\right)$
34 2 7 5 3 frlmelbas ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to \left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in {B}↔\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)\wedge {finSupp}_{{0}_{{R}}}\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\right)\right)\right)$
35 34 adantr ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in {B}↔\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in \left({{\mathrm{Base}}_{{R}}}^{{I}}\right)\wedge {finSupp}_{{0}_{{R}}}\left(\left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\right)\right)\right)$
36 17 33 35 mpbir2and ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\wedge {i}\in {I}\right)\to \left({j}\in {I}⟼if\left({j}={i},{1}_{{R}},{0}_{{R}}\right)\right)\in {B}$
37 6 36 fmpt3d ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {W}\right)\to {U}:{I}⟶{B}$