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

Metamath Proof Explorer

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 → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )