Theorem cnncvsabsnegdemo

Description: Derive the absolute value of a negative complex number absneg to demonstrate the use of the properties of a normed subcomplex vector space for the complex numbers. (Contributed by AV, 9-Oct-2021) (Proof modification is discouraged.)

	Ref	Expression
Assertion	cnncvsabsnegdemo	|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )

Proof

Step	Hyp	Ref	Expression
1		cnfldnm	|- abs = ( norm ` CCfld )
2	1	a1i	|- ( A e. CC -> abs = ( norm ` CCfld ) )
3		cnfldneg	|- ( A e. CC -> ( ( invg ` CCfld ) ` A ) = -u A )
4	3	eqcomd	|- ( A e. CC -> -u A = ( ( invg ` CCfld ) ` A ) )
5	2 4	fveq12d	|- ( A e. CC -> ( abs ` -u A ) = ( ( norm ` CCfld ) ` ( ( invg ` CCfld ) ` A ) ) )
6		cnngp	|- CCfld e. NrmGrp
7		cnfldbas	|- CC = ( Base ` CCfld )
8		eqid	|- ( norm ` CCfld ) = ( norm ` CCfld )
9		eqid	|- ( invg ` CCfld ) = ( invg ` CCfld )
10	7 8 9	nminv	|- ( ( CCfld e. NrmGrp /\ A e. CC ) -> ( ( norm ` CCfld ) ` ( ( invg ` CCfld ) ` A ) ) = ( ( norm ` CCfld ) ` A ) )
11	6 10	mpan	|- ( A e. CC -> ( ( norm ` CCfld ) ` ( ( invg ` CCfld ) ` A ) ) = ( ( norm ` CCfld ) ` A ) )
12	1	eqcomi	|- ( norm ` CCfld ) = abs
13	12	fveq1i	|- ( ( norm ` CCfld ) ` A ) = ( abs ` A )
14	13	a1i	|- ( A e. CC -> ( ( norm ` CCfld ) ` A ) = ( abs ` A ) )
15	5 11 14	3eqtrd	|- ( A e. CC -> ( abs ` -u A ) = ( abs ` A ) )