Definition df-hvsub

Description: Define vector subtraction. See hvsubvali for its value and hvsubcli for its closure. (Contributed by NM, 6-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hvsub	⊢ −ℎ = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmv	⊢ −ℎ
1		vx	⊢ 𝑥
2		chba	⊢ ℋ
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		cva	⊢ +ℎ
6		c1	⊢ 1
7	6	cneg	⊢ - 1
8		csm	⊢ ·ℎ
9	3	cv	⊢ 𝑦
10	7 9 8	co	⊢ ( - 1 ·ℎ 𝑦 )
11	4 10 5	co	⊢ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) )
12	1 3 2 2 11	cmpo	⊢ ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )
13	0 12	wceq	⊢ −ℎ = ( 𝑥 ∈ ℋ , 𝑦 ∈ ℋ ↦ ( 𝑥 +ℎ ( - 1 ·ℎ 𝑦 ) ) )