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

Metamath Proof Explorer

Theorem nvmval

Description: Value of vector subtraction on a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvmval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvmval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvmval.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvmval.3 ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion nvmval ( ( 𝑈 ∈ 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 eqid ⊢ ( /𝑔 ‘ 𝐺 ) = ( /𝑔 ‘ 𝐺 )
9 6 7 8 grpodivval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( /𝑔 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
10 5 9 syl3an1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( /𝑔 ‘ 𝐺 ) 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
11 1 2 4 8 nvm ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 ( /𝑔 ‘ 𝐺 ) 𝐵 ) )
12 1 2 3 7 nvinv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) = ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) )
13 12 3adant2 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) = ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) )
14 13 oveq2d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
15 10 11 14 3eqtr4d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) = ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) )