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}\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}$
frlmssuvc1.l ${⊢}{\phi }\to {L}\in {J}$
frlmssuvc1.x ${⊢}{\phi }\to {X}\in {K}$
Assertion frlmssuvc1

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 frlmssuvc1.l ${⊢}{\phi }\to {L}\in {J}$
12 frlmssuvc1.x ${⊢}{\phi }\to {X}\in {K}$
13 1 frlmlmod ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {F}\in \mathrm{LMod}$
14 8 9 13 syl2anc ${⊢}{\phi }\to {F}\in \mathrm{LMod}$
15 eqid ${⊢}\mathrm{LSubSp}\left({F}\right)=\mathrm{LSubSp}\left({F}\right)$
16 1 15 3 6 7 frlmsslss2 ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\wedge {J}\subseteq {I}\right)\to {C}\in \mathrm{LSubSp}\left({F}\right)$
17 8 9 10 16 syl3anc ${⊢}{\phi }\to {C}\in \mathrm{LSubSp}\left({F}\right)$
18 1 frlmsca ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {R}=\mathrm{Scalar}\left({F}\right)$
19 8 9 18 syl2anc ${⊢}{\phi }\to {R}=\mathrm{Scalar}\left({F}\right)$
20 19 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{R}}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
21 4 20 syl5eq ${⊢}{\phi }\to {K}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
22 12 21 eleqtrd ${⊢}{\phi }\to {X}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
23 2 1 3 uvcff ${⊢}\left({R}\in \mathrm{Ring}\wedge {I}\in {V}\right)\to {U}:{I}⟶{B}$
24 8 9 23 syl2anc ${⊢}{\phi }\to {U}:{I}⟶{B}$
25 10 11 sseldd ${⊢}{\phi }\to {L}\in {I}$
26 24 25 ffvelrnd ${⊢}{\phi }\to {U}\left({L}\right)\in {B}$
27 1 4 3 frlmbasf ${⊢}\left({I}\in {V}\wedge {U}\left({L}\right)\in {B}\right)\to {U}\left({L}\right):{I}⟶{K}$
28 9 26 27 syl2anc ${⊢}{\phi }\to {U}\left({L}\right):{I}⟶{K}$
29 8 adantr ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {R}\in \mathrm{Ring}$
30 9 adantr ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {I}\in {V}$
31 25 adantr ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {L}\in {I}$
32 eldifi ${⊢}{x}\in \left({I}\setminus {J}\right)\to {x}\in {I}$
33 32 adantl ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {x}\in {I}$
34 disjdif ${⊢}{J}\cap \left({I}\setminus {J}\right)=\varnothing$
35 simpr ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {x}\in \left({I}\setminus {J}\right)$
36 disjne ${⊢}\left({J}\cap \left({I}\setminus {J}\right)=\varnothing \wedge {L}\in {J}\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {L}\ne {x}$
37 34 11 35 36 mp3an2ani ${⊢}\left({\phi }\wedge {x}\in \left({I}\setminus {J}\right)\right)\to {L}\ne {x}$
38 2 29 30 31 33 37 6 uvcvv0
39 28 38 suppss
40 oveq1
41 40 sseq1d
42 41 7 elrab2
43 26 39 42 sylanbrc ${⊢}{\phi }\to {U}\left({L}\right)\in {C}$
44 eqid ${⊢}\mathrm{Scalar}\left({F}\right)=\mathrm{Scalar}\left({F}\right)$
45 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({F}\right)}$
46 44 5 45 15 lssvscl
47 14 17 22 43 46 syl22anc