# Metamath Proof Explorer

## Theorem hvmul0or

Description: If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 19-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvmul0or ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}={0}_{ℎ}↔\left({A}=0\vee {B}={0}_{ℎ}\right)\right)$

### Proof

Step Hyp Ref Expression
1 df-ne ${⊢}{A}\ne 0↔¬{A}=0$
2 oveq2 ${⊢}{A}{\cdot }_{ℎ}{B}={0}_{ℎ}\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\left(\frac{1}{{A}}\right){\cdot }_{ℎ}{0}_{ℎ}$
3 2 ad2antlr ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)=\left(\frac{1}{{A}}\right){\cdot }_{ℎ}{0}_{ℎ}$
4 recid2 ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}=1$
5 4 oveq1d ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}{\cdot }_{ℎ}{B}=1{\cdot }_{ℎ}{B}$
6 5 adantlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}{\cdot }_{ℎ}{B}=1{\cdot }_{ℎ}{B}$
7 reccl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{1}{{A}}\in ℂ$
8 7 adantlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to \frac{1}{{A}}\in ℂ$
9 simpll ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to {A}\in ℂ$
10 simplr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to {B}\in ℋ$
11 ax-hvmulass ${⊢}\left(\frac{1}{{A}}\in ℂ\wedge {A}\in ℂ\wedge {B}\in ℋ\right)\to \left(\frac{1}{{A}}\right){A}{\cdot }_{ℎ}{B}=\left(\frac{1}{{A}}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)$
12 8 9 10 11 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){A}{\cdot }_{ℎ}{B}=\left(\frac{1}{{A}}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)$
13 ax-hvmulid ${⊢}{B}\in ℋ\to 1{\cdot }_{ℎ}{B}={B}$
14 13 ad2antlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to 1{\cdot }_{ℎ}{B}={B}$
15 6 12 14 3eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)={B}$
16 15 adantlr ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}\left({A}{\cdot }_{ℎ}{B}\right)={B}$
17 hvmul0 ${⊢}\frac{1}{{A}}\in ℂ\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
18 7 17 syl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
19 18 adantlr ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
20 19 adantlr ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\wedge {A}\ne 0\right)\to \left(\frac{1}{{A}}\right){\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
21 3 16 20 3eqtr3d ${⊢}\left(\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\wedge {A}\ne 0\right)\to {B}={0}_{ℎ}$
22 21 ex ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\to \left({A}\ne 0\to {B}={0}_{ℎ}\right)$
23 1 22 syl5bir ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\to \left(¬{A}=0\to {B}={0}_{ℎ}\right)$
24 23 orrd ${⊢}\left(\left({A}\in ℂ\wedge {B}\in ℋ\right)\wedge {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)\to \left({A}=0\vee {B}={0}_{ℎ}\right)$
25 24 ex ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}={0}_{ℎ}\to \left({A}=0\vee {B}={0}_{ℎ}\right)\right)$
26 ax-hvmul0 ${⊢}{B}\in ℋ\to 0{\cdot }_{ℎ}{B}={0}_{ℎ}$
27 oveq1 ${⊢}{A}=0\to {A}{\cdot }_{ℎ}{B}=0{\cdot }_{ℎ}{B}$
28 27 eqeq1d ${⊢}{A}=0\to \left({A}{\cdot }_{ℎ}{B}={0}_{ℎ}↔0{\cdot }_{ℎ}{B}={0}_{ℎ}\right)$
29 26 28 syl5ibrcom ${⊢}{B}\in ℋ\to \left({A}=0\to {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)$
30 29 adantl ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}=0\to {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)$
31 hvmul0 ${⊢}{A}\in ℂ\to {A}{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}$
32 oveq2 ${⊢}{B}={0}_{ℎ}\to {A}{\cdot }_{ℎ}{B}={A}{\cdot }_{ℎ}{0}_{ℎ}$
33 32 eqeq1d ${⊢}{B}={0}_{ℎ}\to \left({A}{\cdot }_{ℎ}{B}={0}_{ℎ}↔{A}{\cdot }_{ℎ}{0}_{ℎ}={0}_{ℎ}\right)$
34 31 33 syl5ibrcom ${⊢}{A}\in ℂ\to \left({B}={0}_{ℎ}\to {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)$
35 34 adantr ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({B}={0}_{ℎ}\to {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)$
36 30 35 jaod ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left(\left({A}=0\vee {B}={0}_{ℎ}\right)\to {A}{\cdot }_{ℎ}{B}={0}_{ℎ}\right)$
37 25 36 impbid ${⊢}\left({A}\in ℂ\wedge {B}\in ℋ\right)\to \left({A}{\cdot }_{ℎ}{B}={0}_{ℎ}↔\left({A}=0\vee {B}={0}_{ℎ}\right)\right)$