Metamath Proof Explorer


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 AA=A

Proof

Step Hyp Ref Expression
1 cnfldnm abs=normfld
2 1 a1i Aabs=normfld
3 cnfldneg AinvgfldA=A
4 3 eqcomd AA=invgfldA
5 2 4 fveq12d AA=normfldinvgfldA
6 cnngp fldNrmGrp
7 cnfldbas =Basefld
8 eqid normfld=normfld
9 eqid invgfld=invgfld
10 7 8 9 nminv fldNrmGrpAnormfldinvgfldA=normfldA
11 6 10 mpan AnormfldinvgfldA=normfldA
12 1 eqcomi normfld=abs
13 12 fveq1i normfldA=A
14 13 a1i AnormfldA=A
15 5 11 14 3eqtrd AA=A