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	biimtrrid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐴 ·ℎ 𝐵 ) = 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ℎ ) ) )