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

Metamath Proof Explorer

Theorem nvmfval

Description: Value of the function for the vector subtraction operation on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvmval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvmval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvmval.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion nvmfval ( 𝑈 ∈ NrmCVec → 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 nvmval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvmval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 nvmval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 nvmval.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
5 2 nvgrp ⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )
6 1 2 bafval ⊢ 𝑋 = ran 𝐺
7 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
8 2 4 vsfval ⊢ 𝑀 = ( /𝑔 ‘ 𝐺 )
9 6 7 8 grpodivfval ⊢ ( 𝐺 ∈ GrpOp → 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
10 5 9 syl ⊢ ( 𝑈 ∈ NrmCVec → 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
11 1 2 3 7 nvinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑦 ∈ 𝑋 ) → ( - 1 𝑆 𝑦 ) = ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) )
12 11 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( - 1 𝑆 𝑦 ) = ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) )
13 12 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) = ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) )
14 13 mpoeq3dva ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
15 10 14 eqtr4d ⊢ ( 𝑈 ∈ NrmCVec → 𝑀 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( - 1 𝑆 𝑦 ) ) ) )