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=RfreeLModI
frlmssuvc1.u U=RunitVecI
frlmssuvc1.b B=BaseF
frlmssuvc1.k K=BaseR
frlmssuvc1.t ·˙=F
frlmssuvc1.z 0˙=0R
frlmssuvc1.c C=xB|xsupp0˙J
frlmssuvc1.r φRRing
frlmssuvc1.i φIV
frlmssuvc1.j φJI
frlmssuvc2.l φLIJ
frlmssuvc2.x φXK0˙
Assertion frlmssuvc2 φ¬X·˙ULC

Proof

Step Hyp Ref Expression
1 frlmssuvc1.f F=RfreeLModI
2 frlmssuvc1.u U=RunitVecI
3 frlmssuvc1.b B=BaseF
4 frlmssuvc1.k K=BaseR
5 frlmssuvc1.t ·˙=F
6 frlmssuvc1.z 0˙=0R
7 frlmssuvc1.c C=xB|xsupp0˙J
8 frlmssuvc1.r φRRing
9 frlmssuvc1.i φIV
10 frlmssuvc1.j φJI
11 frlmssuvc2.l φLIJ
12 frlmssuvc2.x φXK0˙
13 fveq2 x=LX·˙ULx=X·˙ULL
14 13 neeq1d x=LX·˙ULx0˙X·˙ULL0˙
15 11 eldifad φLI
16 12 eldifad φXK
17 2 1 3 uvcff RRingIVU:IB
18 8 9 17 syl2anc φU:IB
19 18 15 ffvelrnd φULB
20 eqid R=R
21 1 3 4 9 16 19 15 5 20 frlmvscaval φX·˙ULL=XRULL
22 eqid 1R=1R
23 2 8 9 15 22 uvcvv1 φULL=1R
24 23 oveq2d φXRULL=XR1R
25 4 20 22 ringridm RRingXKXR1R=X
26 8 16 25 syl2anc φXR1R=X
27 21 24 26 3eqtrd φX·˙ULL=X
28 eldifsni XK0˙X0˙
29 12 28 syl φX0˙
30 27 29 eqnetrd φX·˙ULL0˙
31 14 15 30 elrabd φLxI|X·˙ULx0˙
32 11 eldifbd φ¬LJ
33 nelss LxI|X·˙ULx0˙¬LJ¬xI|X·˙ULx0˙J
34 31 32 33 syl2anc φ¬xI|X·˙ULx0˙J
35 1 frlmlmod RRingIVFLMod
36 8 9 35 syl2anc φFLMod
37 1 frlmsca RRingIVR=ScalarF
38 8 9 37 syl2anc φR=ScalarF
39 38 fveq2d φBaseR=BaseScalarF
40 4 39 eqtrid φK=BaseScalarF
41 16 40 eleqtrd φXBaseScalarF
42 eqid ScalarF=ScalarF
43 eqid BaseScalarF=BaseScalarF
44 3 42 5 43 lmodvscl FLModXBaseScalarFULBX·˙ULB
45 36 41 19 44 syl3anc φX·˙ULB
46 1 4 3 frlmbasf IVX·˙ULBX·˙UL:IK
47 9 45 46 syl2anc φX·˙UL:IK
48 47 ffnd φX·˙ULFnI
49 6 fvexi 0˙V
50 49 a1i φ0˙V
51 suppvalfn X·˙ULFnIIV0˙VX·˙ULsupp0˙=xI|X·˙ULx0˙
52 48 9 50 51 syl3anc φX·˙ULsupp0˙=xI|X·˙ULx0˙
53 52 sseq1d φX·˙ULsupp0˙JxI|X·˙ULx0˙J
54 34 53 mtbird φ¬X·˙ULsupp0˙J
55 54 intnand φ¬X·˙ULBX·˙ULsupp0˙J
56 oveq1 x=X·˙ULxsupp0˙=X·˙ULsupp0˙
57 56 sseq1d x=X·˙ULxsupp0˙JX·˙ULsupp0˙J
58 57 7 elrab2 X·˙ULCX·˙ULBX·˙ULsupp0˙J
59 55 58 sylnibr φ¬X·˙ULC