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 )
29 8 adantr 
 |-  ( ( ph /\ x e. ( I \ J ) ) -> R e. Ring )
30 9 adantr 
 |-  ( ( ph /\ x e. ( I \ J ) ) -> I e. V )
31 25 adantr 
 |-  ( ( ph /\ x e. ( I \ J ) ) -> L e. I )
32 eldifi 
 |-  ( x e. ( I \ J ) -> x e. I )
33 32 adantl 
 |-  ( ( 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 )