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