Theorem clmabs

Description: Norm in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmabs	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	clmsca	⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
4	3	fveq2d	⊢ ( 𝑊 ∈ ℂMod → ( norm ‘ 𝐹 ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) ) )
5	4	adantr	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( norm ‘ 𝐹 ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) ) )
6	5	fveq1d	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = ( ( norm ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) )
7	1 2	clmsubrg	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
8		subrgsubg	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
9	7 8	syl	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
10		eqid	⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
11		cnfldnm	⊢ abs = ( norm ‘ ℂfld )
12		eqid	⊢ ( norm ‘ ( ℂfld ↾s 𝐾 ) ) = ( norm ‘ ( ℂfld ↾s 𝐾 ) )
13	10 11 12	subgnm2	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ) → ( ( norm ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) = ( abs ‘ 𝐴 ) )
14	9 13	sylan	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( norm ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) = ( abs ‘ 𝐴 ) )
15	6 14	eqtr2d	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( abs ‘ 𝐴 ) = ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) )