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