Theorem cnnvm

Description: The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnnvm.6	|- U = <. <. + , x. >. , abs >.
Assertion	cnnvm	|- - = ( -v ` U )

Proof

Step	Hyp	Ref	Expression
1		cnnvm.6	|- U = <. <. + , x. >. , abs >.
2		mulm1	|- ( y e. CC -> ( -u 1 x. y ) = -u y )
3	2	adantl	|- ( ( x e. CC /\ y e. CC ) -> ( -u 1 x. y ) = -u y )
4	3	oveq2d	|- ( ( x e. CC /\ y e. CC ) -> ( x + ( -u 1 x. y ) ) = ( x + -u y ) )
5		negsub	|- ( ( x e. CC /\ y e. CC ) -> ( x + -u y ) = ( x - y ) )
6	4 5	eqtr2d	|- ( ( x e. CC /\ y e. CC ) -> ( x - y ) = ( x + ( -u 1 x. y ) ) )
7	6	mpoeq3ia	|- ( x e. CC , y e. CC |-> ( x - y ) ) = ( x e. CC , y e. CC |-> ( x + ( -u 1 x. y ) ) )
8		subf	|- - : ( CC X. CC ) --> CC
9		ffn	|- ( - : ( CC X. CC ) --> CC -> - Fn ( CC X. CC ) )
10	8 9	ax-mp	|- - Fn ( CC X. CC )
11		fnov	|- ( - Fn ( CC X. CC ) <-> - = ( x e. CC , y e. CC |-> ( x - y ) ) )
12	10 11	mpbi	|- - = ( x e. CC , y e. CC |-> ( x - y ) )
13	1	cnnv	|- U e. NrmCVec
14	1	cnnvba	|- CC = ( BaseSet ` U )
15	1	cnnvg	|- + = ( +v ` U )
16	1	cnnvs	|- x. = ( .sOLD ` U )
17		eqid	|- ( -v ` U ) = ( -v ` U )
18	14 15 16 17	nvmfval	|- ( U e. NrmCVec -> ( -v ` U ) = ( x e. CC , y e. CC |-> ( x + ( -u 1 x. y ) ) ) )
19	13 18	ax-mp	|- ( -v ` U ) = ( x e. CC , y e. CC |-> ( x + ( -u 1 x. y ) ) )
20	7 12 19	3eqtr4i	|- - = ( -v ` U )