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	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( abs ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		cnfldnm	⊢ abs = ( norm ‘ ℂfld )
2	1	a1i	⊢ ( 𝐴 ∈ ℂ → abs = ( norm ‘ ℂfld ) )
3		cnfldneg	⊢ ( 𝐴 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
4	3	eqcomd	⊢ ( 𝐴 ∈ ℂ → - 𝐴 = ( ( invg ‘ ℂfld ) ‘ 𝐴 ) )
5	2 4	fveq12d	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( ( norm ‘ ℂfld ) ‘ ( ( invg ‘ ℂfld ) ‘ 𝐴 ) ) )
6		cnngp	⊢ ℂfld ∈ NrmGrp
7		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
8		eqid	⊢ ( norm ‘ ℂfld ) = ( norm ‘ ℂfld )
9		eqid	⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
10	7 8 9	nminv	⊢ ( ( ℂfld ∈ NrmGrp ∧ 𝐴 ∈ ℂ ) → ( ( norm ‘ ℂfld ) ‘ ( ( invg ‘ ℂfld ) ‘ 𝐴 ) ) = ( ( norm ‘ ℂfld ) ‘ 𝐴 ) )
11	6 10	mpan	⊢ ( 𝐴 ∈ ℂ → ( ( norm ‘ ℂfld ) ‘ ( ( invg ‘ ℂfld ) ‘ 𝐴 ) ) = ( ( norm ‘ ℂfld ) ‘ 𝐴 ) )
12	1	eqcomi	⊢ ( norm ‘ ℂfld ) = abs
13	12	fveq1i	⊢ ( ( norm ‘ ℂfld ) ‘ 𝐴 ) = ( abs ‘ 𝐴 )
14	13	a1i	⊢ ( 𝐴 ∈ ℂ → ( ( norm ‘ ℂfld ) ‘ 𝐴 ) = ( abs ‘ 𝐴 ) )
15	5 11 14	3eqtrd	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ - 𝐴 ) = ( abs ‘ 𝐴 ) )