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. ) ) )