# 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}=\mathrm{BaseSet}\left({U}\right)$
nvmul0or.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
nvmul0or.6 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
Assertion nvmul0or ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to \left({A}{S}{B}={Z}↔\left({A}=0\vee {B}={Z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 nvmul0or.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvmul0or.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
3 nvmul0or.6 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
4 df-ne ${⊢}{A}\ne 0↔¬{A}=0$
5 oveq2 ${⊢}{A}{S}{B}={Z}\to \left(\frac{1}{{A}}\right){S}\left({A}{S}{B}\right)=\left(\frac{1}{{A}}\right){S}{Z}$
6 5 ad2antlr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){S}\left({A}{S}{B}\right)=\left(\frac{1}{{A}}\right){S}{Z}$
7 recid2 ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}=1$
8 7 oveq1d ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}{S}{B}=1{S}{B}$
9 8 3ad2antl2 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}{S}{B}=1{S}{B}$
10 simpl1 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to {U}\in \mathrm{NrmCVec}$
11 reccl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{1}{{A}}\in ℂ$
12 11 3ad2antl2 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to \frac{1}{{A}}\in ℂ$
13 simpl2 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to {A}\in ℂ$
14 simpl3 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to {B}\in {X}$
15 1 2 nvsass ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left(\frac{1}{{A}}\in ℂ\wedge {A}\in ℂ\wedge {B}\in {X}\right)\right)\to \left(\frac{1}{{A}}\right){A}{S}{B}=\left(\frac{1}{{A}}\right){S}\left({A}{S}{B}\right)$
16 10 12 13 14 15 syl13anc ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}{S}{B}=\left(\frac{1}{{A}}\right){S}\left({A}{S}{B}\right)$
17 1 2 nvsid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to 1{S}{B}={B}$
18 17 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to 1{S}{B}={B}$
19 18 adantr ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to 1{S}{B}={B}$
20 9 16 19 3eqtr3d ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){S}\left({A}{S}{B}\right)={B}$
21 20 adantlr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){S}\left({A}{S}{B}\right)={B}$
22 2 3 nvsz ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \frac{1}{{A}}\in ℂ\right)\to \left(\frac{1}{{A}}\right){S}{Z}={Z}$
23 11 22 sylan2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge \left({A}\in ℂ\wedge {A}\ne 0\right)\right)\to \left(\frac{1}{{A}}\right){S}{Z}={Z}$
24 23 anassrs ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){S}{Z}={Z}$
25 24 3adantl3 ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){S}{Z}={Z}$
26 25 adantlr ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){S}{Z}={Z}$
27 6 21 26 3eqtr3d ${⊢}\left(\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\wedge {A}\ne 0\right)\to {B}={Z}$
28 27 ex ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\to \left({A}\ne 0\to {B}={Z}\right)$
29 4 28 syl5bir ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\to \left(¬{A}=0\to {B}={Z}\right)$
30 29 orrd ${⊢}\left(\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\wedge {A}{S}{B}={Z}\right)\to \left({A}=0\vee {B}={Z}\right)$
31 30 ex ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to \left({A}{S}{B}={Z}\to \left({A}=0\vee {B}={Z}\right)\right)$
32 1 2 3 nv0 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to 0{S}{B}={Z}$
33 oveq1 ${⊢}{A}=0\to {A}{S}{B}=0{S}{B}$
34 33 eqeq1d ${⊢}{A}=0\to \left({A}{S}{B}={Z}↔0{S}{B}={Z}\right)$
35 32 34 syl5ibrcom ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {B}\in {X}\right)\to \left({A}=0\to {A}{S}{B}={Z}\right)$
36 35 3adant2 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to \left({A}=0\to {A}{S}{B}={Z}\right)$
37 2 3 nvsz ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\right)\to {A}{S}{Z}={Z}$
38 oveq2 ${⊢}{B}={Z}\to {A}{S}{B}={A}{S}{Z}$
39 38 eqeq1d ${⊢}{B}={Z}\to \left({A}{S}{B}={Z}↔{A}{S}{Z}={Z}\right)$
40 37 39 syl5ibrcom ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\right)\to \left({B}={Z}\to {A}{S}{B}={Z}\right)$
41 40 3adant3 ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to \left({B}={Z}\to {A}{S}{B}={Z}\right)$
42 36 41 jaod ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to \left(\left({A}=0\vee {B}={Z}\right)\to {A}{S}{B}={Z}\right)$
43 31 42 impbid ${⊢}\left({U}\in \mathrm{NrmCVec}\wedge {A}\in ℂ\wedge {B}\in {X}\right)\to \left({A}{S}{B}={Z}↔\left({A}=0\vee {B}={Z}\right)\right)$