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}=\mathrm{Scalar}\left({W}\right)$
clmsub.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
Assertion clmabs ${⊢}\left({W}\in \mathrm{CMod}\wedge {A}\in {K}\right)\to \left|{A}\right|=\mathrm{norm}\left({F}\right)\left({A}\right)$

Proof

Step Hyp Ref Expression
1 clm0.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 clmsub.k ${⊢}{K}={\mathrm{Base}}_{{F}}$
3 1 2 clmsca ${⊢}{W}\in \mathrm{CMod}\to {F}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}$
4 3 fveq2d ${⊢}{W}\in \mathrm{CMod}\to \mathrm{norm}\left({F}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)$
5 4 adantr ${⊢}\left({W}\in \mathrm{CMod}\wedge {A}\in {K}\right)\to \mathrm{norm}\left({F}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)$
6 5 fveq1d ${⊢}\left({W}\in \mathrm{CMod}\wedge {A}\in {K}\right)\to \mathrm{norm}\left({F}\right)\left({A}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)\left({A}\right)$
7 1 2 clmsubrg ${⊢}{W}\in \mathrm{CMod}\to {K}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
8 subrgsubg ${⊢}{K}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to {K}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
9 7 8 syl ${⊢}{W}\in \mathrm{CMod}\to {K}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
10 eqid ${⊢}{ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}$
11 cnfldnm ${⊢}\mathrm{abs}=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}\right)$
12 eqid ${⊢}\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)=\mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)$
13 10 11 12 subgnm2 ${⊢}\left({K}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge {A}\in {K}\right)\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)\left({A}\right)=\left|{A}\right|$
14 9 13 sylan ${⊢}\left({W}\in \mathrm{CMod}\wedge {A}\in {K}\right)\to \mathrm{norm}\left({ℂ}_{\mathrm{fld}}{↾}_{𝑠}{K}\right)\left({A}\right)=\left|{A}\right|$
15 6 14 eqtr2d ${⊢}\left({W}\in \mathrm{CMod}\wedge {A}\in {K}\right)\to \left|{A}\right|=\mathrm{norm}\left({F}\right)\left({A}\right)$