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 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝑀 𝐵 ) = 𝑍 ↔ 𝐴 = 𝐵 ) )