Metamath Proof Explorer

Theorem nvmul0or

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

Ref Expression
Hypotheses nvmul0or.1 ⊢ X = BaseSet ⁡ U
nvmul0or.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvmul0or.6 ⊢ Z = 0 vec ⁡ U
Assertion nvmul0or ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → A S B = Z ↔ A = 0 ∨ B = Z

Proof

Step Hyp Ref Expression
1 nvmul0or.1 ⊢ X = BaseSet ⁡ U
2 nvmul0or.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
3 nvmul0or.6 ⊢ Z = 0 vec ⁡ U
4 df-ne ⊢ A ≠ 0 ↔ ¬ A = 0
5 oveq2 ⊢ A S B = Z → 1 A S A S B = 1 A S Z
6 5 ad2antlr ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z ∧ A ≠ 0 → 1 A S A S B = 1 A S Z
7 recid2 ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ⁢ A = 1
8 7 oveq1d ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ⁢ A S B = 1 S B
9 8 3ad2antl2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → 1 A ⁢ A S B = 1 S B
10 simpl1 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → U ∈ NrmCVec
11 reccl ⊢ A ∈ ℂ ∧ A ≠ 0 → 1 A ∈ ℂ
12 11 3ad2antl2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → 1 A ∈ ℂ
13 simpl2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → A ∈ ℂ
14 simpl3 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → B ∈ X
15 1 2 nvsass ⊢ U ∈ NrmCVec ∧ 1 A ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ X → 1 A ⁢ A S B = 1 A S A S B
16 10 12 13 14 15 syl13anc ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → 1 A ⁢ A S B = 1 A S A S B
17 1 2 nvsid ⊢ U ∈ NrmCVec ∧ B ∈ X → 1 S B = B
18 17 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → 1 S B = B
19 18 adantr ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → 1 S B = B
20 9 16 19 3eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → 1 A S A S B = B
21 20 adantlr ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z ∧ A ≠ 0 → 1 A S A S B = B
22 2 3 nvsz ⊢ U ∈ NrmCVec ∧ 1 A ∈ ℂ → 1 A S Z = Z
23 11 22 sylan2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ A ≠ 0 → 1 A S Z = Z
24 23 anassrs ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ A ≠ 0 → 1 A S Z = Z
25 24 3adantl3 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A ≠ 0 → 1 A S Z = Z
26 25 adantlr ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z ∧ A ≠ 0 → 1 A S Z = Z
27 6 21 26 3eqtr3d ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z ∧ A ≠ 0 → B = Z
28 27 ex ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z → A ≠ 0 → B = Z
29 4 28 syl5bir ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z → ¬ A = 0 → B = Z
30 29 orrd ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X ∧ A S B = Z → A = 0 ∨ B = Z
31 30 ex ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → A S B = Z → A = 0 ∨ B = Z
32 1 2 3 nv0 ⊢ U ∈ NrmCVec ∧ B ∈ X → 0 S B = Z
33 oveq1 ⊢ A = 0 → A S B = 0 S B
34 33 eqeq1d ⊢ A = 0 → A S B = Z ↔ 0 S B = Z
35 32 34 syl5ibrcom ⊢ U ∈ NrmCVec ∧ B ∈ X → A = 0 → A S B = Z
36 35 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → A = 0 → A S B = Z
37 2 3 nvsz ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → A S Z = Z
38 oveq2 ⊢ B = Z → A S B = A S Z
39 38 eqeq1d ⊢ B = Z → A S B = Z ↔ A S Z = Z
40 37 39 syl5ibrcom ⊢ U ∈ NrmCVec ∧ A ∈ ℂ → B = Z → A S B = Z
41 40 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → B = Z → A S B = Z
42 36 41 jaod ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → A = 0 ∨ B = Z → A S B = Z
43 31 42 impbid ⊢ U ∈ NrmCVec ∧ A ∈ ℂ ∧ B ∈ X → A S B = Z ↔ A = 0 ∨ B = Z