Metamath Proof Explorer


Theorem lvecvsn0

Description: A scalar product is nonzero iff both of its factors are nonzero. (Contributed by NM, 3-Jan-2015)

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 lvecvsn0
|- ( 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 1 2 3 4 5 6 7 8 9 lvecvs0or
 |-  ( ph -> ( ( A .x. X ) = .0. <-> ( A = O \/ X = .0. ) ) )
11 10 necon3abid
 |-  ( ph -> ( ( A .x. X ) =/= .0. <-> -. ( A = O \/ X = .0. ) ) )
12 neanior
 |-  ( ( A =/= O /\ X =/= .0. ) <-> -. ( A = O \/ X = .0. ) )
13 11 12 bitr4di
 |-  ( ph -> ( ( A .x. X ) =/= .0. <-> ( A =/= O /\ X =/= .0. ) ) )