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\in ℂ\to \left|-A\right|=\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		cnfldnm	$$⊢\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	a1i	$$⊢A\in ℂ\to \mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
3		cnfldneg	$$⊢A\in ℂ\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=-A$$
4	3	eqcomd	$$⊢A\in ℂ\to -A={inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)$$
5	2 4	fveq12d	$$⊢A\in ℂ\to \left|-A\right|=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left({inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)\right)$$
6		cnngp	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}$$
7		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
8		eqid	$$⊢\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$$
9		eqid	$$⊢{inv}_g\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)$$
10	7 8 9	nminv	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{NrmGrp}\wedge A\in ℂ\right)\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left({inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)$$
11	6 10	mpan	$$⊢A\in ℂ\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left({inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)$$
12	1	eqcomi	$$⊢\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{abs}$$
13	12	fveq1i	$$⊢\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=\left|A\right|$$
14	13	a1i	$$⊢A\in ℂ\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)\left(A\right)=\left|A\right|$$
15	5 11 14	3eqtrd	$$⊢A\in ℂ\to \left|-A\right|=\left|A\right|$$