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 ⊢ X = BaseSet ⁡ U
nvmval.2 ⊢ G = + v ⁡ U
nvmval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvmval.3 ⊢ M = - v ⁡ U
Assertion nvmfval ⊢ U ∈ NrmCVec → M = x ∈ X , y ∈ X ⟼ x G -1 S y

Proof

Step Hyp Ref Expression
1 nvmval.1 ⊢ X = BaseSet ⁡ U
2 nvmval.2 ⊢ G = + v ⁡ U
3 nvmval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 nvmval.3 ⊢ M = - v ⁡ U
5 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
6 1 2 bafval ⊢ X = ran ⁡ G
7 eqid ⊢ inv ⁡ G = inv ⁡ G
8 2 4 vsfval ⊢ M = / g ⁡ G
9 6 7 8 grpodivfval ⊢ G ∈ GrpOp → M = x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y
10 5 9 syl ⊢ U ∈ NrmCVec → M = x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y
11 1 2 3 7 nvinv ⊢ U ∈ NrmCVec ∧ y ∈ X → -1 S y = inv ⁡ G ⁡ y
12 11 3adant2 ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → -1 S y = inv ⁡ G ⁡ y
13 12 oveq2d ⊢ U ∈ NrmCVec ∧ x ∈ X ∧ y ∈ X → x G -1 S y = x G inv ⁡ G ⁡ y
14 13 mpoeq3dva ⊢ U ∈ NrmCVec → x ∈ X , y ∈ X ⟼ x G -1 S y = x ∈ X , y ∈ X ⟼ x G inv ⁡ G ⁡ y
15 10 14 eqtr4d ⊢ U ∈ NrmCVec → M = x ∈ X , y ∈ X ⟼ x G -1 S y