Theorem nvmf

Description: Mapping for the vector subtraction operation. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvmf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvmf.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion	nvmf	⊢ ( 𝑈 ∈ NrmCVec → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		nvmf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvmf.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		simpl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑈 ∈ NrmCVec )
4		simprl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
5		neg1cn	⊢ - 1 ∈ ℂ
6		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
7	1 6	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝑦 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ 𝑋 )
8	5 7	mp3an2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ 𝑋 )
9	8	adantrl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ 𝑋 )
10		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
11	1 10	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ∈ 𝑋 ) → ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ∈ 𝑋 )
12	3 4 9 11	syl3anc	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ∈ 𝑋 )
13	12	ralrimivva	⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ∈ 𝑋 )
14		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) )
15	14	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ∈ 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
16	13 15	sylib	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
17	1 10 6 2	nvmfval	⊢ ( 𝑈 ∈ NrmCVec → 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) )
18	17	feq1d	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 ( +𝑣 ‘ 𝑈 ) ( - 1 ( ·𝑠OLD ‘ 𝑈 ) 𝑦 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
19	16 18	mpbird	⊢ ( 𝑈 ∈ NrmCVec → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )