# Metamath Proof Explorer

## Theorem frlmssuvc2

Description: A nonzero scalar multiple of a unit vector not included in a support-restriction subspace is not 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 )`
frlmssuvc2.l
`|- ( ph -> L e. ( I \ J ) )`
frlmssuvc2.x
`|- ( ph -> X e. ( K \ { .0. } ) )`
Assertion frlmssuvc2
`|- ( 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 frlmssuvc2.l
` |-  ( ph -> L e. ( I \ J ) )`
12 frlmssuvc2.x
` |-  ( ph -> X e. ( K \ { .0. } ) )`
13 fveq2
` |-  ( x = L -> ( ( X .x. ( U ` L ) ) ` x ) = ( ( X .x. ( U ` L ) ) ` L ) )`
14 13 neeq1d
` |-  ( x = L -> ( ( ( X .x. ( U ` L ) ) ` x ) =/= .0. <-> ( ( X .x. ( U ` L ) ) ` L ) =/= .0. ) )`
` |-  ( ph -> L e. I )`
` |-  ( ph -> X e. K )`
17 2 1 3 uvcff
` |-  ( ( R e. Ring /\ I e. V ) -> U : I --> B )`
18 8 9 17 syl2anc
` |-  ( ph -> U : I --> B )`
19 18 15 ffvelrnd
` |-  ( ph -> ( U ` L ) e. B )`
20 eqid
` |-  ( .r ` R ) = ( .r ` R )`
21 1 3 4 9 16 19 15 5 20 frlmvscaval
` |-  ( ph -> ( ( X .x. ( U ` L ) ) ` L ) = ( X ( .r ` R ) ( ( U ` L ) ` L ) ) )`
22 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
23 2 8 9 15 22 uvcvv1
` |-  ( ph -> ( ( U ` L ) ` L ) = ( 1r ` R ) )`
24 23 oveq2d
` |-  ( ph -> ( X ( .r ` R ) ( ( U ` L ) ` L ) ) = ( X ( .r ` R ) ( 1r ` R ) ) )`
25 4 20 22 ringridm
` |-  ( ( R e. Ring /\ X e. K ) -> ( X ( .r ` R ) ( 1r ` R ) ) = X )`
26 8 16 25 syl2anc
` |-  ( ph -> ( X ( .r ` R ) ( 1r ` R ) ) = X )`
27 21 24 26 3eqtrd
` |-  ( ph -> ( ( X .x. ( U ` L ) ) ` L ) = X )`
28 eldifsni
` |-  ( X e. ( K \ { .0. } ) -> X =/= .0. )`
29 12 28 syl
` |-  ( ph -> X =/= .0. )`
30 27 29 eqnetrd
` |-  ( ph -> ( ( X .x. ( U ` L ) ) ` L ) =/= .0. )`
31 14 15 30 elrabd
` |-  ( ph -> L e. { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } )`
32 11 eldifbd
` |-  ( ph -> -. L e. J )`
33 nelss
` |-  ( ( L e. { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } /\ -. L e. J ) -> -. { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } C_ J )`
34 31 32 33 syl2anc
` |-  ( ph -> -. { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } C_ J )`
35 1 frlmlmod
` |-  ( ( R e. Ring /\ I e. V ) -> F e. LMod )`
36 8 9 35 syl2anc
` |-  ( ph -> F e. LMod )`
37 1 frlmsca
` |-  ( ( R e. Ring /\ I e. V ) -> R = ( Scalar ` F ) )`
38 8 9 37 syl2anc
` |-  ( ph -> R = ( Scalar ` F ) )`
39 38 fveq2d
` |-  ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` F ) ) )`
40 4 39 syl5eq
` |-  ( ph -> K = ( Base ` ( Scalar ` F ) ) )`
41 16 40 eleqtrd
` |-  ( ph -> X e. ( Base ` ( Scalar ` F ) ) )`
42 eqid
` |-  ( Scalar ` F ) = ( Scalar ` F )`
43 eqid
` |-  ( Base ` ( Scalar ` F ) ) = ( Base ` ( Scalar ` F ) )`
44 3 42 5 43 lmodvscl
` |-  ( ( F e. LMod /\ X e. ( Base ` ( Scalar ` F ) ) /\ ( U ` L ) e. B ) -> ( X .x. ( U ` L ) ) e. B )`
45 36 41 19 44 syl3anc
` |-  ( ph -> ( X .x. ( U ` L ) ) e. B )`
46 1 4 3 frlmbasf
` |-  ( ( I e. V /\ ( X .x. ( U ` L ) ) e. B ) -> ( X .x. ( U ` L ) ) : I --> K )`
47 9 45 46 syl2anc
` |-  ( ph -> ( X .x. ( U ` L ) ) : I --> K )`
48 47 ffnd
` |-  ( ph -> ( X .x. ( U ` L ) ) Fn I )`
49 6 fvexi
` |-  .0. e. _V`
50 49 a1i
` |-  ( ph -> .0. e. _V )`
51 suppvalfn
` |-  ( ( ( X .x. ( U ` L ) ) Fn I /\ I e. V /\ .0. e. _V ) -> ( ( X .x. ( U ` L ) ) supp .0. ) = { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } )`
52 48 9 50 51 syl3anc
` |-  ( ph -> ( ( X .x. ( U ` L ) ) supp .0. ) = { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } )`
53 52 sseq1d
` |-  ( ph -> ( ( ( X .x. ( U ` L ) ) supp .0. ) C_ J <-> { x e. I | ( ( X .x. ( U ` L ) ) ` x ) =/= .0. } C_ J ) )`
54 34 53 mtbird
` |-  ( ph -> -. ( ( X .x. ( U ` L ) ) supp .0. ) C_ J )`
55 54 intnand
` |-  ( ph -> -. ( ( X .x. ( U ` L ) ) e. B /\ ( ( X .x. ( U ` L ) ) supp .0. ) C_ J ) )`
56 oveq1
` |-  ( x = ( X .x. ( U ` L ) ) -> ( x supp .0. ) = ( ( X .x. ( U ` L ) ) supp .0. ) )`
57 56 sseq1d
` |-  ( x = ( X .x. ( U ` L ) ) -> ( ( x supp .0. ) C_ J <-> ( ( X .x. ( U ` L ) ) supp .0. ) C_ J ) )`
58 57 7 elrab2
` |-  ( ( X .x. ( U ` L ) ) e. C <-> ( ( X .x. ( U ` L ) ) e. B /\ ( ( X .x. ( U ` L ) ) supp .0. ) C_ J ) )`
59 55 58 sylnibr
` |-  ( ph -> -. ( X .x. ( U ` L ) ) e. C )`