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 = ( Base ` W )`
lssvs0or.t
`|- .x. = ( .s ` W )`
lssvs0or.f
`|- F = ( Scalar ` W )`
lssvs0or.k
`|- K = ( Base ` F )`
lssvs0or.o
`|- .0. = ( 0g ` F )`
lssvs0or.s
`|- S = ( LSubSp ` W )`
lssvs0or.w
`|- ( ph -> W e. LVec )`
lssvs0or.u
`|- ( ph -> U e. S )`
lssvs0or.x
`|- ( ph -> X e. V )`
lssvs0or.a
`|- ( ph -> A e. K )`
Assertion lssvs0or
`|- ( ph -> ( ( A .x. X ) e. U <-> ( A = .0. \/ X e. U ) ) )`

Proof

Step Hyp Ref Expression
1 lssvs0or.v
` |-  V = ( Base ` W )`
2 lssvs0or.t
` |-  .x. = ( .s ` W )`
3 lssvs0or.f
` |-  F = ( Scalar ` W )`
4 lssvs0or.k
` |-  K = ( Base ` F )`
5 lssvs0or.o
` |-  .0. = ( 0g ` F )`
6 lssvs0or.s
` |-  S = ( LSubSp ` W )`
7 lssvs0or.w
` |-  ( ph -> W e. LVec )`
8 lssvs0or.u
` |-  ( ph -> U e. S )`
9 lssvs0or.x
` |-  ( ph -> X e. V )`
10 lssvs0or.a
` |-  ( ph -> A e. K )`
11 3 lvecdrng
` |-  ( W e. LVec -> F e. DivRing )`
12 7 11 syl
` |-  ( ph -> F e. DivRing )`
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> F e. DivRing )`
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> A e. K )`
15 simpr
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> A =/= .0. )`
16 eqid
` |-  ( .r ` F ) = ( .r ` F )`
17 eqid
` |-  ( 1r ` F ) = ( 1r ` F )`
18 eqid
` |-  ( invr ` F ) = ( invr ` F )`
19 4 5 16 17 18 drnginvrl
` |-  ( ( F e. DivRing /\ A e. K /\ A =/= .0. ) -> ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) = ( 1r ` F ) )`
20 13 14 15 19 syl3anc
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) = ( 1r ` F ) )`
21 20 oveq1d
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) .x. X ) = ( ( 1r ` F ) .x. X ) )`
22 lveclmod
` |-  ( W e. LVec -> W e. LMod )`
23 7 22 syl
` |-  ( ph -> W e. LMod )`
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> W e. LMod )`
25 4 5 18 drnginvrcl
` |-  ( ( F e. DivRing /\ A e. K /\ A =/= .0. ) -> ( ( invr ` F ) ` A ) e. K )`
26 13 14 15 25 syl3anc
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( ( invr ` F ) ` A ) e. K )`
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> X e. V )`
28 1 3 2 4 16 lmodvsass
` |-  ( ( W e. LMod /\ ( ( ( invr ` F ) ` A ) e. K /\ A e. K /\ X e. V ) ) -> ( ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) .x. X ) = ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) )`
29 24 26 14 27 28 syl13anc
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) .x. X ) = ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) )`
30 1 3 2 17 lmodvs1
` |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )`
31 24 27 30 syl2anc
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( ( 1r ` F ) .x. X ) = X )`
32 21 29 31 3eqtr3rd
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> X = ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) )`
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> U e. S )`
34 simplr
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( A .x. X ) e. U )`
35 3 2 4 6 lssvscl
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( ( ( invr ` F ) ` A ) e. K /\ ( A .x. X ) e. U ) ) -> ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) e. U )`
36 24 33 26 34 35 syl22anc
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) e. U )`
37 32 36 eqeltrd
` |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> X e. U )`
38 37 ex
` |-  ( ( ph /\ ( A .x. X ) e. U ) -> ( A =/= .0. -> X e. U ) )`
39 38 necon1bd
` |-  ( ( ph /\ ( A .x. X ) e. U ) -> ( -. X e. U -> A = .0. ) )`
40 39 orrd
` |-  ( ( ph /\ ( A .x. X ) e. U ) -> ( X e. U \/ A = .0. ) )`
41 40 orcomd
` |-  ( ( ph /\ ( A .x. X ) e. U ) -> ( A = .0. \/ X e. U ) )`
42 oveq1
` |-  ( A = .0. -> ( A .x. X ) = ( .0. .x. X ) )`
` |-  ( ( ph /\ A = .0. ) -> ( A .x. X ) = ( .0. .x. X ) )`
44 eqid
` |-  ( 0g ` W ) = ( 0g ` W )`
45 1 3 2 5 44 lmod0vs
` |-  ( ( W e. LMod /\ X e. V ) -> ( .0. .x. X ) = ( 0g ` W ) )`
46 23 9 45 syl2anc
` |-  ( ph -> ( .0. .x. X ) = ( 0g ` W ) )`
47 44 6 lss0cl
` |-  ( ( W e. LMod /\ U e. S ) -> ( 0g ` W ) e. U )`
48 23 8 47 syl2anc
` |-  ( ph -> ( 0g ` W ) e. U )`
49 46 48 eqeltrd
` |-  ( ph -> ( .0. .x. X ) e. U )`
` |-  ( ( ph /\ A = .0. ) -> ( .0. .x. X ) e. U )`
51 43 50 eqeltrd
` |-  ( ( ph /\ A = .0. ) -> ( A .x. X ) e. U )`
` |-  ( ( ph /\ X e. U ) -> W e. LMod )`
` |-  ( ( ph /\ X e. U ) -> U e. S )`
` |-  ( ( ph /\ X e. U ) -> A e. K )`
` |-  ( ( ph /\ X e. U ) -> X e. U )`
` |-  ( ( ( W e. LMod /\ U e. S ) /\ ( A e. K /\ X e. U ) ) -> ( A .x. X ) e. U )`
` |-  ( ( ph /\ X e. U ) -> ( A .x. X ) e. U )`
` |-  ( ( ph /\ ( A = .0. \/ X e. U ) ) -> ( A .x. X ) e. U )`
` |-  ( ph -> ( ( A .x. X ) e. U <-> ( A = .0. \/ X e. U ) ) )`