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 ffvelcdmd 
 |-  ( 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 eqtrid 
 |-  ( 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 )