Metamath Proof Explorer


Theorem lvecvs0or

Description: If a scalar product is zero, one of its factors must be zero. ( hvmul0or analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lvecmul0or.v
|- V = ( Base ` W )
lvecmul0or.s
|- .x. = ( .s ` W )
lvecmul0or.f
|- F = ( Scalar ` W )
lvecmul0or.k
|- K = ( Base ` F )
lvecmul0or.o
|- O = ( 0g ` F )
lvecmul0or.z
|- .0. = ( 0g ` W )
lvecmul0or.w
|- ( ph -> W e. LVec )
lvecmul0or.a
|- ( ph -> A e. K )
lvecmul0or.x
|- ( ph -> X e. V )
Assertion lvecvs0or
|- ( ph -> ( ( A .x. X ) = .0. <-> ( A = O \/ X = .0. ) ) )

Proof

Step Hyp Ref Expression
1 lvecmul0or.v
 |-  V = ( Base ` W )
2 lvecmul0or.s
 |-  .x. = ( .s ` W )
3 lvecmul0or.f
 |-  F = ( Scalar ` W )
4 lvecmul0or.k
 |-  K = ( Base ` F )
5 lvecmul0or.o
 |-  O = ( 0g ` F )
6 lvecmul0or.z
 |-  .0. = ( 0g ` W )
7 lvecmul0or.w
 |-  ( ph -> W e. LVec )
8 lvecmul0or.a
 |-  ( ph -> A e. K )
9 lvecmul0or.x
 |-  ( ph -> X e. V )
10 df-ne
 |-  ( A =/= O <-> -. A = O )
11 oveq2
 |-  ( ( A .x. X ) = .0. -> ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) = ( ( ( invr ` F ) ` A ) .x. .0. ) )
12 11 ad2antlr
 |-  ( ( ( ph /\ ( A .x. X ) = .0. ) /\ A =/= O ) -> ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) = ( ( ( invr ` F ) ` A ) .x. .0. ) )
13 7 adantr
 |-  ( ( ph /\ A =/= O ) -> W e. LVec )
14 3 lvecdrng
 |-  ( W e. LVec -> F e. DivRing )
15 13 14 syl
 |-  ( ( ph /\ A =/= O ) -> F e. DivRing )
16 8 adantr
 |-  ( ( ph /\ A =/= O ) -> A e. K )
17 simpr
 |-  ( ( ph /\ A =/= O ) -> A =/= O )
18 eqid
 |-  ( .r ` F ) = ( .r ` F )
19 eqid
 |-  ( 1r ` F ) = ( 1r ` F )
20 eqid
 |-  ( invr ` F ) = ( invr ` F )
21 4 5 18 19 20 drnginvrl
 |-  ( ( F e. DivRing /\ A e. K /\ A =/= O ) -> ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) = ( 1r ` F ) )
22 15 16 17 21 syl3anc
 |-  ( ( ph /\ A =/= O ) -> ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) = ( 1r ` F ) )
23 22 oveq1d
 |-  ( ( ph /\ A =/= O ) -> ( ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) .x. X ) = ( ( 1r ` F ) .x. X ) )
24 lveclmod
 |-  ( W e. LVec -> W e. LMod )
25 7 24 syl
 |-  ( ph -> W e. LMod )
26 25 adantr
 |-  ( ( ph /\ A =/= O ) -> W e. LMod )
27 4 5 20 drnginvrcl
 |-  ( ( F e. DivRing /\ A e. K /\ A =/= O ) -> ( ( invr ` F ) ` A ) e. K )
28 15 16 17 27 syl3anc
 |-  ( ( ph /\ A =/= O ) -> ( ( invr ` F ) ` A ) e. K )
29 9 adantr
 |-  ( ( ph /\ A =/= O ) -> X e. V )
30 1 3 2 4 18 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 ) ) )
31 26 28 16 29 30 syl13anc
 |-  ( ( ph /\ A =/= O ) -> ( ( ( ( invr ` F ) ` A ) ( .r ` F ) A ) .x. X ) = ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) )
32 1 3 2 19 lmodvs1
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )
33 25 9 32 syl2anc
 |-  ( ph -> ( ( 1r ` F ) .x. X ) = X )
34 33 adantr
 |-  ( ( ph /\ A =/= O ) -> ( ( 1r ` F ) .x. X ) = X )
35 23 31 34 3eqtr3d
 |-  ( ( ph /\ A =/= O ) -> ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) = X )
36 35 adantlr
 |-  ( ( ( ph /\ ( A .x. X ) = .0. ) /\ A =/= O ) -> ( ( ( invr ` F ) ` A ) .x. ( A .x. X ) ) = X )
37 25 adantr
 |-  ( ( ph /\ ( A .x. X ) = .0. ) -> W e. LMod )
38 37 adantr
 |-  ( ( ( ph /\ ( A .x. X ) = .0. ) /\ A =/= O ) -> W e. LMod )
39 28 adantlr
 |-  ( ( ( ph /\ ( A .x. X ) = .0. ) /\ A =/= O ) -> ( ( invr ` F ) ` A ) e. K )
40 3 2 4 6 lmodvs0
 |-  ( ( W e. LMod /\ ( ( invr ` F ) ` A ) e. K ) -> ( ( ( invr ` F ) ` A ) .x. .0. ) = .0. )
41 38 39 40 syl2anc
 |-  ( ( ( ph /\ ( A .x. X ) = .0. ) /\ A =/= O ) -> ( ( ( invr ` F ) ` A ) .x. .0. ) = .0. )
42 12 36 41 3eqtr3d
 |-  ( ( ( ph /\ ( A .x. X ) = .0. ) /\ A =/= O ) -> X = .0. )
43 42 ex
 |-  ( ( ph /\ ( A .x. X ) = .0. ) -> ( A =/= O -> X = .0. ) )
44 10 43 syl5bir
 |-  ( ( ph /\ ( A .x. X ) = .0. ) -> ( -. A = O -> X = .0. ) )
45 44 orrd
 |-  ( ( ph /\ ( A .x. X ) = .0. ) -> ( A = O \/ X = .0. ) )
46 45 ex
 |-  ( ph -> ( ( A .x. X ) = .0. -> ( A = O \/ X = .0. ) ) )
47 1 3 2 5 6 lmod0vs
 |-  ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) = .0. )
48 25 9 47 syl2anc
 |-  ( ph -> ( O .x. X ) = .0. )
49 oveq1
 |-  ( A = O -> ( A .x. X ) = ( O .x. X ) )
50 49 eqeq1d
 |-  ( A = O -> ( ( A .x. X ) = .0. <-> ( O .x. X ) = .0. ) )
51 48 50 syl5ibrcom
 |-  ( ph -> ( A = O -> ( A .x. X ) = .0. ) )
52 3 2 4 6 lmodvs0
 |-  ( ( W e. LMod /\ A e. K ) -> ( A .x. .0. ) = .0. )
53 25 8 52 syl2anc
 |-  ( ph -> ( A .x. .0. ) = .0. )
54 oveq2
 |-  ( X = .0. -> ( A .x. X ) = ( A .x. .0. ) )
55 54 eqeq1d
 |-  ( X = .0. -> ( ( A .x. X ) = .0. <-> ( A .x. .0. ) = .0. ) )
56 53 55 syl5ibrcom
 |-  ( ph -> ( X = .0. -> ( A .x. X ) = .0. ) )
57 51 56 jaod
 |-  ( ph -> ( ( A = O \/ X = .0. ) -> ( A .x. X ) = .0. ) )
58 46 57 impbid
 |-  ( ph -> ( ( A .x. X ) = .0. <-> ( A = O \/ X = .0. ) ) )