Metamath Proof Explorer

Theorem lssvs0or

Description: If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015)

Ref Expression
Hypotheses lssvs0or.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
lssvs0or.t
lssvs0or.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
lssvs0or.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
lssvs0or.o
lssvs0or.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
lssvs0or.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
lssvs0or.u ${⊢}{\phi }\to {U}\in {S}$
lssvs0or.x ${⊢}{\phi }\to {X}\in {V}$
lssvs0or.a ${⊢}{\phi }\to {A}\in {K}$
Assertion lssvs0or

Proof

Step Hyp Ref Expression
1 lssvs0or.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
2 lssvs0or.t
3 lssvs0or.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
4 lssvs0or.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
5 lssvs0or.o
6 lssvs0or.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
7 lssvs0or.w ${⊢}{\phi }\to {W}\in \mathrm{LVec}$
8 lssvs0or.u ${⊢}{\phi }\to {U}\in {S}$
9 lssvs0or.x ${⊢}{\phi }\to {X}\in {V}$
10 lssvs0or.a ${⊢}{\phi }\to {A}\in {K}$
11 3 lvecdrng ${⊢}{W}\in \mathrm{LVec}\to {F}\in \mathrm{DivRing}$
12 7 11 syl ${⊢}{\phi }\to {F}\in \mathrm{DivRing}$
15 simpr
16 eqid ${⊢}{\cdot }_{{F}}={\cdot }_{{F}}$
17 eqid ${⊢}{1}_{{F}}={1}_{{F}}$
18 eqid ${⊢}{inv}_{r}\left({F}\right)={inv}_{r}\left({F}\right)$
19 4 5 16 17 18 drnginvrl
20 13 14 15 19 syl3anc
21 20 oveq1d
22 lveclmod ${⊢}{W}\in \mathrm{LVec}\to {W}\in \mathrm{LMod}$
23 7 22 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
25 4 5 18 drnginvrcl
26 13 14 15 25 syl3anc
28 1 3 2 4 16 lmodvsass
29 24 26 14 27 28 syl13anc
30 1 3 2 17 lmodvs1
31 24 27 30 syl2anc
32 21 29 31 3eqtr3rd
34 simplr
35 3 2 4 6 lssvscl
36 24 33 26 34 35 syl22anc
37 32 36 eqeltrd
38 37 ex
39 38 necon1bd
40 39 orrd
41 40 orcomd
42 oveq1
44 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
45 1 3 2 5 44 lmod0vs
46 23 9 45 syl2anc
47 44 6 lss0cl ${⊢}\left({W}\in \mathrm{LMod}\wedge {U}\in {S}\right)\to {0}_{{W}}\in {U}$
48 23 8 47 syl2anc ${⊢}{\phi }\to {0}_{{W}}\in {U}$
49 46 48 eqeltrd
52 23 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {W}\in \mathrm{LMod}$
53 8 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {U}\in {S}$
54 10 adantr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {A}\in {K}$
55 simpr ${⊢}\left({\phi }\wedge {X}\in {U}\right)\to {X}\in {U}$