This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nvmeq0

Description: The difference between two vectors is zero iff they are equal. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvmeq0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmeq0.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
nvmeq0.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
Assertion nvmeq0 ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑀 𝐵 ) = 𝑍 ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 nvmeq0.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvmeq0.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 nvmeq0.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
4 1 2 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 )
5 4 3expb ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 )
6 1 3 nvzcl ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 ∈ 𝑋 )
7 6 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑍 ∈ 𝑋 )
8 simprr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
9 5 7 8 3jca ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
10 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
11 1 10 nvrcan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 ∧ 𝑍 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝑀 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐵 ) = ( 𝑍 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ↔ ( 𝐴 𝑀 𝐵 ) = 𝑍 ) )
12 9 11 syldan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝑀 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐵 ) = ( 𝑍 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ↔ ( 𝐴 𝑀 𝐵 ) = 𝑍 ) )
13 12 3impb ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 𝑀 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐵 ) = ( 𝑍 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ↔ ( 𝐴 𝑀 𝐵 ) = 𝑍 ) )
14 1 10 2 nvnpcan ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑀 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐵 ) = 𝐴 )
15 1 10 3 nv0lid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( 𝑍 ( +𝑣 ‘ 𝑈 ) 𝐵 ) = 𝐵 )
16 15 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑍 ( +𝑣 ‘ 𝑈 ) 𝐵 ) = 𝐵 )
17 14 16 eqeq12d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 𝑀 𝐵 ) ( +𝑣 ‘ 𝑈 ) 𝐵 ) = ( 𝑍 ( +𝑣 ‘ 𝑈 ) 𝐵 ) ↔ 𝐴 = 𝐵 ) )
18 13 17 bitr3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑀 𝐵 ) = 𝑍 ↔ 𝐴 = 𝐵 ) )