Theorem nvmid

Description: A vector minus itself is the zero vector. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nvmeq0.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvmeq0.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		nvmeq0.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
4		eqid	⊢ 𝐴 = 𝐴
5	1 2 3	nvmeq0	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝑀 𝐴 ) = 𝑍 ↔ 𝐴 = 𝐴 ) )
6	5	3anidm23	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 𝑀 𝐴 ) = 𝑍 ↔ 𝐴 = 𝐴 ) )
7	4 6	mpbiri	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐴 ) = 𝑍 )