Description: If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nvmul0or.1 | |
|
nvmul0or.4 | |
||
nvmul0or.6 | |
||
Assertion | nvmul0or | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nvmul0or.1 | |
|
2 | nvmul0or.4 | |
|
3 | nvmul0or.6 | |
|
4 | df-ne | |
|
5 | oveq2 | |
|
6 | 5 | ad2antlr | |
7 | recid2 | |
|
8 | 7 | oveq1d | |
9 | 8 | 3ad2antl2 | |
10 | simpl1 | |
|
11 | reccl | |
|
12 | 11 | 3ad2antl2 | |
13 | simpl2 | |
|
14 | simpl3 | |
|
15 | 1 2 | nvsass | |
16 | 10 12 13 14 15 | syl13anc | |
17 | 1 2 | nvsid | |
18 | 17 | 3adant2 | |
19 | 18 | adantr | |
20 | 9 16 19 | 3eqtr3d | |
21 | 20 | adantlr | |
22 | 2 3 | nvsz | |
23 | 11 22 | sylan2 | |
24 | 23 | anassrs | |
25 | 24 | 3adantl3 | |
26 | 25 | adantlr | |
27 | 6 21 26 | 3eqtr3d | |
28 | 27 | ex | |
29 | 4 28 | syl5bir | |
30 | 29 | orrd | |
31 | 30 | ex | |
32 | 1 2 3 | nv0 | |
33 | oveq1 | |
|
34 | 33 | eqeq1d | |
35 | 32 34 | syl5ibrcom | |
36 | 35 | 3adant2 | |
37 | 2 3 | nvsz | |
38 | oveq2 | |
|
39 | 38 | eqeq1d | |
40 | 37 39 | syl5ibrcom | |
41 | 40 | 3adant3 | |
42 | 36 41 | jaod | |
43 | 31 42 | impbid | |