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

Metamath Proof Explorer

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 ·_ℎ 𝑦 ) ) )