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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmul0or.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvmul0or.6 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
Assertion nvmul0or ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) = 𝑍 ↔ ( 𝐴 = 0 ∨ 𝐵 = 𝑍 ) ) )

Proof

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