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}\mathrm{freeLMod}{I}$
frlmssuvc1.u ${⊢}{U}={R}\mathrm{unitVec}{I}$
frlmssuvc1.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
frlmssuvc1.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
frlmssuvc1.t
frlmssuvc1.z
frlmssuvc1.c
frlmssuvc1.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
frlmssuvc1.i ${⊢}{\phi }\to {I}\in {V}$
frlmssuvc1.j ${⊢}{\phi }\to {J}\subseteq {I}$
frlmssuvc2.l ${⊢}{\phi }\to {L}\in \left({I}\setminus {J}\right)$
frlmssuvc2.x
Assertion frlmssuvc2

Proof

Step Hyp Ref Expression
1 frlmssuvc1.f ${⊢}{F}={R}\mathrm{freeLMod}{I}$
2 frlmssuvc1.u ${⊢}{U}={R}\mathrm{unitVec}{I}$
3 frlmssuvc1.b ${⊢}{B}={\mathrm{Base}}_{{F}}$
4 frlmssuvc1.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
5 frlmssuvc1.t
6 frlmssuvc1.z
7 frlmssuvc1.c
8 frlmssuvc1.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
9 frlmssuvc1.i ${⊢}{\phi }\to {I}\in {V}$
10 frlmssuvc1.j ${⊢}{\phi }\to {J}\subseteq {I}$
11 frlmssuvc2.l ${⊢}{\phi }\to {L}\in \left({I}\setminus {J}\right)$
12 frlmssuvc2.x
13 fveq2
14 13 neeq1d
15 11 eldifad ${⊢}{\phi }\to {L}\in {I}$
16 12 eldifad ${⊢}{\phi }\to {X}\in {K}$
17 2 1 3 uvcff ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {U}:{I}⟶{B}$
18 8 9 17 syl2anc ${⊢}{\phi }\to {U}:{I}⟶{B}$
19 18 15 ffvelrnd ${⊢}{\phi }\to {U}\left({L}\right)\in {B}$
20 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
21 1 3 4 9 16 19 15 5 20 frlmvscaval
22 eqid ${⊢}{1}_{{R}}={1}_{{R}}$
23 2 8 9 15 22 uvcvv1 ${⊢}{\phi }\to {U}\left({L}\right)\left({L}\right)={1}_{{R}}$
24 23 oveq2d ${⊢}{\phi }\to {X}{\cdot }_{{R}}{U}\left({L}\right)\left({L}\right)={X}{\cdot }_{{R}}{1}_{{R}}$
25 4 20 22 ringridm ${⊢}\left({R}\in \mathrm{Ring}\wedge {X}\in {K}\right)\to {X}{\cdot }_{{R}}{1}_{{R}}={X}$
26 8 16 25 syl2anc ${⊢}{\phi }\to {X}{\cdot }_{{R}}{1}_{{R}}={X}$
27 21 24 26 3eqtrd
28 eldifsni
29 12 28 syl
30 27 29 eqnetrd
31 14 15 30 elrabd
32 11 eldifbd ${⊢}{\phi }\to ¬{L}\in {J}$
33 nelss
34 31 32 33 syl2anc
35 1 frlmlmod ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {F}\in \mathrm{LMod}$
36 8 9 35 syl2anc ${⊢}{\phi }\to {F}\in \mathrm{LMod}$
37 1 frlmsca ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {R}=\mathrm{Scalar}\left({F}\right)$
38 8 9 37 syl2anc ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({F}\right)$
39 38 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
40 4 39 syl5eq ${⊢}{\phi }\to {K}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
41 16 40 eleqtrd ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
42 eqid ${⊢}\mathrm{Scalar}\left({F}\right)=\mathrm{Scalar}\left({F}\right)$
43 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
44 3 42 5 43 lmodvscl
45 36 41 19 44 syl3anc
46 1 4 3 frlmbasf
47 9 45 46 syl2anc
48 47 ffnd
49 6 fvexi
50 49 a1i
51 suppvalfn
52 48 9 50 51 syl3anc
53 52 sseq1d
54 34 53 mtbird
55 54 intnand
56 oveq1
57 56 sseq1d
58 57 7 elrab2
59 55 58 sylnibr