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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ℎ 𝐵 ) = 0ℎ ↔ ( 𝐴 = 0 ∨ 𝐵 = 0ℎ ) ) )

Proof

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