Metamath Proof Explorer

Theorem clmabs

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

Ref Expression
Hypotheses clm0.f ⊢ F = Scalar ⁡ W
clmsub.k ⊢ K = Base F
Assertion clmabs ⊢ W ∈ CMod ∧ A ∈ K → A = norm ⁡ F ⁡ A

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ F = Scalar ⁡ W
2 clmsub.k ⊢ K = Base F
3 1 2 clmsca ⊢ W ∈ CMod → F = ℂ fld ↾ 𝑠 K
4 3 fveq2d ⊢ W ∈ CMod → norm ⁡ F = norm ⁡ ℂ fld ↾ 𝑠 K
5 4 adantr ⊢ W ∈ CMod ∧ A ∈ K → norm ⁡ F = norm ⁡ ℂ fld ↾ 𝑠 K
6 5 fveq1d ⊢ W ∈ CMod ∧ A ∈ K → norm ⁡ F ⁡ A = norm ⁡ ℂ fld ↾ 𝑠 K ⁡ A
7 1 2 clmsubrg ⊢ W ∈ CMod → K ∈ SubRing ⁡ ℂ fld
8 subrgsubg ⊢ K ∈ SubRing ⁡ ℂ fld → K ∈ SubGrp ⁡ ℂ fld
9 7 8 syl ⊢ W ∈ CMod → K ∈ SubGrp ⁡ ℂ fld
10 eqid ⊢ ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 K
11 cnfldnm ⊢ abs = norm ⁡ ℂ fld
12 eqid ⊢ norm ⁡ ℂ fld ↾ 𝑠 K = norm ⁡ ℂ fld ↾ 𝑠 K
13 10 11 12 subgnm2 ⊢ K ∈ SubGrp ⁡ ℂ fld ∧ A ∈ K → norm ⁡ ℂ fld ↾ 𝑠 K ⁡ A = A
14 9 13 sylan ⊢ W ∈ CMod ∧ A ∈ K → norm ⁡ ℂ fld ↾ 𝑠 K ⁡ A = A
15 6 14 eqtr2d ⊢ W ∈ CMod ∧ A ∈ K → A = norm ⁡ F ⁡ A