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. ) )
15 11 eldifad
 |-  ( ph -> L e. I )
16 12 eldifad
 |-  ( 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 )