# Metamath Proof Explorer

## Theorem frlmssuvc1

Description: A scalar multiple of a unit vector included in a support-restriction subspace is included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 24-Jun-2019)

Ref Expression
Hypotheses frlmssuvc1.f
`|- F = ( R freeLMod I )`
frlmssuvc1.u
`|- U = ( R unitVec I )`
frlmssuvc1.b
`|- B = ( Base ` F )`
frlmssuvc1.k
`|- K = ( Base ` R )`
frlmssuvc1.t
`|- .x. = ( .s ` F )`
frlmssuvc1.z
`|- .0. = ( 0g ` R )`
frlmssuvc1.c
`|- C = { x e. B | ( x supp .0. ) C_ J }`
frlmssuvc1.r
`|- ( ph -> R e. Ring )`
frlmssuvc1.i
`|- ( ph -> I e. V )`
frlmssuvc1.j
`|- ( ph -> J C_ I )`
frlmssuvc1.l
`|- ( ph -> L e. J )`
frlmssuvc1.x
`|- ( ph -> X e. K )`
Assertion frlmssuvc1
`|- ( ph -> ( X .x. ( U ` L ) ) e. C )`

### Proof

Step Hyp Ref Expression
1 frlmssuvc1.f
` |-  F = ( R freeLMod I )`
2 frlmssuvc1.u
` |-  U = ( R unitVec I )`
3 frlmssuvc1.b
` |-  B = ( Base ` F )`
4 frlmssuvc1.k
` |-  K = ( Base ` R )`
5 frlmssuvc1.t
` |-  .x. = ( .s ` F )`
6 frlmssuvc1.z
` |-  .0. = ( 0g ` R )`
7 frlmssuvc1.c
` |-  C = { x e. B | ( x supp .0. ) C_ J }`
8 frlmssuvc1.r
` |-  ( ph -> R e. Ring )`
9 frlmssuvc1.i
` |-  ( ph -> I e. V )`
10 frlmssuvc1.j
` |-  ( ph -> J C_ I )`
11 frlmssuvc1.l
` |-  ( ph -> L e. J )`
12 frlmssuvc1.x
` |-  ( ph -> X e. K )`
13 1 frlmlmod
` |-  ( ( R e. Ring /\ I e. V ) -> F e. LMod )`
14 8 9 13 syl2anc
` |-  ( ph -> F e. LMod )`
15 eqid
` |-  ( LSubSp ` F ) = ( LSubSp ` F )`
16 1 15 3 6 7 frlmsslss2
` |-  ( ( R e. Ring /\ I e. V /\ J C_ I ) -> C e. ( LSubSp ` F ) )`
17 8 9 10 16 syl3anc
` |-  ( ph -> C e. ( LSubSp ` F ) )`
18 1 frlmsca
` |-  ( ( R e. Ring /\ I e. V ) -> R = ( Scalar ` F ) )`
19 8 9 18 syl2anc
` |-  ( ph -> R = ( Scalar ` F ) )`
20 19 fveq2d
` |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )`
21 4 20 syl5eq
` |-  ( ph -> K = ( Base ` ( Scalar ` F ) ) )`
22 12 21 eleqtrd
` |-  ( ph -> X e. ( Base ` ( Scalar ` F ) ) )`
23 2 1 3 uvcff
` |-  ( ( R e. Ring /\ I e. V ) -> U : I --> B )`
24 8 9 23 syl2anc
` |-  ( ph -> U : I --> B )`
25 10 11 sseldd
` |-  ( ph -> L e. I )`
26 24 25 ffvelrnd
` |-  ( ph -> ( U ` L ) e. B )`
27 1 4 3 frlmbasf
` |-  ( ( I e. V /\ ( U ` L ) e. B ) -> ( U ` L ) : I --> K )`
28 9 26 27 syl2anc
` |-  ( ph -> ( U ` L ) : I --> K )`
` |-  ( ( ph /\ x e. ( I \ J ) ) -> R e. Ring )`
` |-  ( ( ph /\ x e. ( I \ J ) ) -> I e. V )`
` |-  ( ( ph /\ x e. ( I \ J ) ) -> L e. I )`
32 eldifi
` |-  ( x e. ( I \ J ) -> x e. I )`
` |-  ( ( ph /\ x e. ( I \ J ) ) -> x e. I )`
34 disjdif
` |-  ( J i^i ( I \ J ) ) = (/)`
35 simpr
` |-  ( ( ph /\ x e. ( I \ J ) ) -> x e. ( I \ J ) )`
36 disjne
` |-  ( ( ( J i^i ( I \ J ) ) = (/) /\ L e. J /\ x e. ( I \ J ) ) -> L =/= x )`
37 34 11 35 36 mp3an2ani
` |-  ( ( ph /\ x e. ( I \ J ) ) -> L =/= x )`
38 2 29 30 31 33 37 6 uvcvv0
` |-  ( ( ph /\ x e. ( I \ J ) ) -> ( ( U ` L ) ` x ) = .0. )`
39 28 38 suppss
` |-  ( ph -> ( ( U ` L ) supp .0. ) C_ J )`
40 oveq1
` |-  ( x = ( U ` L ) -> ( x supp .0. ) = ( ( U ` L ) supp .0. ) )`
41 40 sseq1d
` |-  ( x = ( U ` L ) -> ( ( x supp .0. ) C_ J <-> ( ( U ` L ) supp .0. ) C_ J ) )`
42 41 7 elrab2
` |-  ( ( U ` L ) e. C <-> ( ( U ` L ) e. B /\ ( ( U ` L ) supp .0. ) C_ J ) )`
43 26 39 42 sylanbrc
` |-  ( ph -> ( U ` L ) e. C )`
44 eqid
` |-  ( Scalar ` F ) = ( Scalar ` F )`
45 eqid
` |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )`
46 44 5 45 15 lssvscl
` |-  ( ( ( F e. LMod /\ C e. ( LSubSp ` F ) ) /\ ( X e. ( Base ` ( Scalar ` F ) ) /\ ( U ` L ) e. C ) ) -> ( X .x. ( U ` L ) ) e. C )`
47 14 17 22 43 46 syl22anc
` |-  ( ph -> ( X .x. ( U ` L ) ) e. C )`