Metamath Proof Explorer


Theorem nvmul0or

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 X=BaseSetU
nvmul0or.4 S=𝑠OLDU
nvmul0or.6 Z=0vecU
Assertion nvmul0or UNrmCVecABXASB=ZA=0B=Z

Proof

Step Hyp Ref Expression
1 nvmul0or.1 X=BaseSetU
2 nvmul0or.4 S=𝑠OLDU
3 nvmul0or.6 Z=0vecU
4 df-ne A0¬A=0
5 oveq2 ASB=Z1ASASB=1ASZ
6 5 ad2antlr UNrmCVecABXASB=ZA01ASASB=1ASZ
7 recid2 AA01AA=1
8 7 oveq1d AA01AASB=1SB
9 8 3ad2antl2 UNrmCVecABXA01AASB=1SB
10 simpl1 UNrmCVecABXA0UNrmCVec
11 reccl AA01A
12 11 3ad2antl2 UNrmCVecABXA01A
13 simpl2 UNrmCVecABXA0A
14 simpl3 UNrmCVecABXA0BX
15 1 2 nvsass UNrmCVec1AABX1AASB=1ASASB
16 10 12 13 14 15 syl13anc UNrmCVecABXA01AASB=1ASASB
17 1 2 nvsid UNrmCVecBX1SB=B
18 17 3adant2 UNrmCVecABX1SB=B
19 18 adantr UNrmCVecABXA01SB=B
20 9 16 19 3eqtr3d UNrmCVecABXA01ASASB=B
21 20 adantlr UNrmCVecABXASB=ZA01ASASB=B
22 2 3 nvsz UNrmCVec1A1ASZ=Z
23 11 22 sylan2 UNrmCVecAA01ASZ=Z
24 23 anassrs UNrmCVecAA01ASZ=Z
25 24 3adantl3 UNrmCVecABXA01ASZ=Z
26 25 adantlr UNrmCVecABXASB=ZA01ASZ=Z
27 6 21 26 3eqtr3d UNrmCVecABXASB=ZA0B=Z
28 27 ex UNrmCVecABXASB=ZA0B=Z
29 4 28 syl5bir UNrmCVecABXASB=Z¬A=0B=Z
30 29 orrd UNrmCVecABXASB=ZA=0B=Z
31 30 ex UNrmCVecABXASB=ZA=0B=Z
32 1 2 3 nv0 UNrmCVecBX0SB=Z
33 oveq1 A=0ASB=0SB
34 33 eqeq1d A=0ASB=Z0SB=Z
35 32 34 syl5ibrcom UNrmCVecBXA=0ASB=Z
36 35 3adant2 UNrmCVecABXA=0ASB=Z
37 2 3 nvsz UNrmCVecAASZ=Z
38 oveq2 B=ZASB=ASZ
39 38 eqeq1d B=ZASB=ZASZ=Z
40 37 39 syl5ibrcom UNrmCVecAB=ZASB=Z
41 40 3adant3 UNrmCVecABXB=ZASB=Z
42 36 41 jaod UNrmCVecABXA=0B=ZASB=Z
43 31 42 impbid UNrmCVecABXASB=ZA=0B=Z