# 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 unitVec I )`
uvcff.y
`|- Y = ( R freeLMod I )`
uvcff.b
`|- B = ( Base ` Y )`
Assertion uvcff
`|- ( ( R e. Ring /\ I e. W ) -> U : I --> B )`

### Proof

Step Hyp Ref Expression
1 uvcff.u
` |-  U = ( R unitVec I )`
2 uvcff.y
` |-  Y = ( R freeLMod I )`
3 uvcff.b
` |-  B = ( Base ` Y )`
4 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
5 eqid
` |-  ( 0g ` R ) = ( 0g ` R )`
6 1 4 5 uvcfval
` |-  ( ( R e. Ring /\ I e. W ) -> U = ( i e. I |-> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) ) )`
7 eqid
` |-  ( Base ` R ) = ( Base ` R )`
8 7 4 ringidcl
` |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )`
9 7 5 ring0cl
` |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )`
10 8 9 ifcld
` |-  ( R e. Ring -> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )`
` |-  ( ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) /\ j e. I ) -> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) e. ( Base ` R ) )`
12 11 fmpttd
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) : I --> ( Base ` R ) )`
13 fvex
` |-  ( Base ` R ) e. _V`
14 elmapg
` |-  ( ( ( Base ` R ) e. _V /\ I e. W ) -> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) : I --> ( Base ` R ) ) )`
15 13 14 mpan
` |-  ( I e. W -> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) : I --> ( Base ` R ) ) )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) : I --> ( Base ` R ) ) )`
17 12 16 mpbird
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m I ) )`
18 mptexg
` |-  ( I e. W -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V )`
20 funmpt
` |-  Fun ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) )`
21 20 a1i
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> Fun ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) )`
22 fvex
` |-  ( 0g ` R ) e. _V`
23 22 a1i
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( 0g ` R ) e. _V )`
24 snfi
` |-  { i } e. Fin`
25 24 a1i
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> { i } e. Fin )`
26 eldifsni
` |-  ( j e. ( I \ { i } ) -> j =/= i )`
` |-  ( ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) /\ j e. ( I \ { i } ) ) -> j =/= i )`
28 27 neneqd
` |-  ( ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) /\ j e. ( I \ { i } ) ) -> -. j = i )`
29 28 iffalsed
` |-  ( ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) /\ j e. ( I \ { i } ) ) -> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )`
30 simplr
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> I e. W )`
31 29 30 suppss2
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { i } )`
32 suppssfifsupp
` |-  ( ( ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { i } e. Fin /\ ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { i } ) ) -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) )`
33 19 21 23 25 31 32 syl32anc
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) )`
34 2 7 5 3 frlmelbas
` |-  ( ( R e. Ring /\ I e. W ) -> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. B <-> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m I ) /\ ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) ) )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. B <-> ( ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m I ) /\ ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) ) ) )`
` |-  ( ( ( R e. Ring /\ I e. W ) /\ i e. I ) -> ( j e. I |-> if ( j = i , ( 1r ` R ) , ( 0g ` R ) ) ) e. B )`
` |-  ( ( R e. Ring /\ I e. W ) -> U : I --> B )`