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 ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B = 0 ℎ ↔ A = 0 ∨ B = 0 ℎ

Proof

Step Hyp Ref Expression
1 df-ne ⊢ A ≠ 0 ↔ ¬ A = 0
2 oveq2 ⊢ A ⋅ ℎ B = 0 ℎ → 1 A ⋅ ℎ A ⋅ ℎ B = 1 A ⋅ ℎ 0 ℎ
3 2 ad2antlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ ∧ A ≠ 0 → 1 A ⋅ ℎ A ⋅ ℎ B = 1 A ⋅ ℎ 0 ℎ
4 recid2 ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ⁢ A = 1
5 4 oveq1d ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ⁢ A ⋅ ℎ B = 1 ⋅ ℎ B
6 5 adantlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → 1 A ⁢ A ⋅ ℎ B = 1 ⋅ ℎ B
7 reccl ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ∈ ℂ
8 7 adantlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → 1 A ∈ ℂ
9 simpll ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → A ∈ ℂ
10 simplr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → B ∈ ℋ
11 ax-hvmulass ⊢ 1 A ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℋ → 1 A ⁢ A ⋅ ℎ B = 1 A ⋅ ℎ A ⋅ ℎ B
12 8 9 10 11 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → 1 A ⁢ A ⋅ ℎ B = 1 A ⋅ ℎ A ⋅ ℎ B
13 ax-hvmulid ⊢ B ∈ ℋ → 1 ⋅ ℎ B = B
14 13 ad2antlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → 1 ⋅ ℎ B = B
15 6 12 14 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → 1 A ⋅ ℎ A ⋅ ℎ B = B
16 15 adantlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ ∧ A ≠ 0 → 1 A ⋅ ℎ A ⋅ ℎ B = B
17 hvmul0 ⊢ 1 A ∈ ℂ → 1 A ⋅ ℎ 0 ℎ = 0 ℎ
18 7 17 syl ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ⋅ ℎ 0 ℎ = 0 ℎ
19 18 adantlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ≠ 0 → 1 A ⋅ ℎ 0 ℎ = 0 ℎ
20 19 adantlr ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ ∧ A ≠ 0 → 1 A ⋅ ℎ 0 ℎ = 0 ℎ
21 3 16 20 3eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ ∧ A ≠ 0 → B = 0 ℎ
22 21 ex ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ → A ≠ 0 → B = 0 ℎ
23 1 22 biimtrrid ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ → ¬ A = 0 → B = 0 ℎ
24 23 orrd ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ A ⋅ ℎ B = 0 ℎ → A = 0 ∨ B = 0 ℎ
25 24 ex ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B = 0 ℎ → A = 0 ∨ B = 0 ℎ
26 ax-hvmul0 ⊢ B ∈ ℋ → 0 ⋅ ℎ B = 0 ℎ
27 oveq1 ⊢ A = 0 → A ⋅ ℎ B = 0 ⋅ ℎ B
28 27 eqeq1d ⊢ A = 0 → A ⋅ ℎ B = 0 ℎ ↔ 0 ⋅ ℎ B = 0 ℎ
29 26 28 syl5ibrcom ⊢ B ∈ ℋ → A = 0 → A ⋅ ℎ B = 0 ℎ
30 29 adantl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A = 0 → A ⋅ ℎ B = 0 ℎ
31 hvmul0 ⊢ A ∈ ℂ → A ⋅ ℎ 0 ℎ = 0 ℎ
32 oveq2 ⊢ B = 0 ℎ → A ⋅ ℎ B = A ⋅ ℎ 0 ℎ
33 32 eqeq1d ⊢ B = 0 ℎ → A ⋅ ℎ B = 0 ℎ ↔ A ⋅ ℎ 0 ℎ = 0 ℎ
34 31 33 syl5ibrcom ⊢ A ∈ ℂ → B = 0 ℎ → A ⋅ ℎ B = 0 ℎ
35 34 adantr ⊢ A ∈ ℂ ∧ B ∈ ℋ → B = 0 ℎ → A ⋅ ℎ B = 0 ℎ
36 30 35 jaod ⊢ A ∈ ℂ ∧ B ∈ ℋ → A = 0 ∨ B = 0 ℎ → A ⋅ ℎ B = 0 ℎ
37 25 36 impbid ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B = 0 ℎ ↔ A = 0 ∨ B = 0 ℎ