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 )
13 12 ad2antrr 
 |-  ( ( ( ph /\ ( A .x. X ) e. U ) /\ A =/= .0. ) -> F e. DivRing )
14 10 ad2antrr 
 |-  ( ( ( 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 )
24 23 ad2antrr 
 |-  ( ( ( 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 )
27 9 ad2antrr 
 |-  ( ( ( 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 ) ) )
33 8 ad2antrr 
 |-  ( ( ( 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 ) )
43 42 adantl 
 |-  ( ( 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 )
50 49 adantr 
 |-  ( ( ph /\ A = .0. ) -> ( .0. .x. X ) e. U )
51 43 50 eqeltrd 
 |-  ( ( ph /\ A = .0. ) -> ( A .x. X ) e. U )
52 23 adantr 
 |-  ( ( ph /\ X e. U ) -> W e. LMod )
53 8 adantr 
 |-  ( ( ph /\ X e. U ) -> U e. S )
54 10 adantr 
 |-  ( ( ph /\ X e. U ) -> A e. K )
55 simpr 
 |-  ( ( ph /\ X e. U ) -> X e. U )
56 3 2 4 6 lssvscl 
 |-  ( ( ( W e. LMod /\ U e. S ) /\ ( A e. K /\ X e. U ) ) -> ( A .x. X ) e. U )
57 52 53 54 55 56 syl22anc 
 |-  ( ( ph /\ X e. U ) -> ( A .x. X ) e. U )
58 51 57 jaodan 
 |-  ( ( ph /\ ( A = .0. \/ X e. U ) ) -> ( A .x. X ) e. U )
59 41 58 impbida 
 |-  ( ph -> ( ( A .x. X ) e. U <-> ( A = .0. \/ X e. U ) ) )