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ℎ→1A⋅ℎA⋅ℎB=1A⋅ℎ0ℎ
3 2 ad2antlr ⊢A∈ℂ∧B∈ℋ∧A⋅ℎB=0ℎ∧A≠0→1A⋅ℎA⋅ℎB=1A⋅ℎ0ℎ
4 recid2 ⊢A∈ℂ∧A≠0→1A⁢A=1
5 4 oveq1d ⊢A∈ℂ∧A≠0→1A⁢A⋅ℎB=1⋅ℎB
6 5 adantlr ⊢A∈ℂ∧B∈ℋ∧A≠0→1A⁢A⋅ℎB=1⋅ℎB
7 reccl ⊢A∈ℂ∧A≠0→1A∈ℂ
8 7 adantlr ⊢A∈ℂ∧B∈ℋ∧A≠0→1A∈ℂ
9 simpll ⊢A∈ℂ∧B∈ℋ∧A≠0→A∈ℂ
10 simplr ⊢A∈ℂ∧B∈ℋ∧A≠0→B∈ℋ
11 ax-hvmulass ⊢1A∈ℂ∧A∈ℂ∧B∈ℋ→1A⁢A⋅ℎB=1A⋅ℎA⋅ℎB
12 8 9 10 11 syl3anc ⊢A∈ℂ∧B∈ℋ∧A≠0→1A⁢A⋅ℎB=1A⋅ℎ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→1A⋅ℎA⋅ℎB=B
16 15 adantlr ⊢A∈ℂ∧B∈ℋ∧A⋅ℎB=0ℎ∧A≠0→1A⋅ℎA⋅ℎB=B
17 hvmul0 ⊢1A∈ℂ→1A⋅ℎ0ℎ=0ℎ
18 7 17 syl ⊢A∈ℂ∧A≠0→1A⋅ℎ0ℎ=0ℎ
19 18 adantlr ⊢A∈ℂ∧B∈ℋ∧A≠0→1A⋅ℎ0ℎ=0ℎ
20 19 adantlr ⊢A∈ℂ∧B∈ℋ∧A⋅ℎB=0ℎ∧A≠0→1A⋅ℎ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ℎ