This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmcj

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

Ref Expression
Hypothesis clm0.f ⊢ F = Scalar ⁡ W
Assertion clmcj ⊢ W ∈ CMod → * = * F

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ F = Scalar ⁡ W
2 fvex ⊢ Base F ∈ V
3 eqid ⊢ ℂ fld ↾ 𝑠 Base F = ℂ fld ↾ 𝑠 Base F
4 cnfldcj ⊢ * = * ℂ fld
5 3 4 ressstarv ⊢ Base F ∈ V → * = * ℂ fld ↾ 𝑠 Base F
6 2 5 ax-mp ⊢ * = * ℂ fld ↾ 𝑠 Base F
7 eqid ⊢ Base F = Base F
8 1 7 clmsca ⊢ W ∈ CMod → F = ℂ fld ↾ 𝑠 Base F
9 8 fveq2d ⊢ W ∈ CMod → * F = * ℂ fld ↾ 𝑠 Base F
10 6 9 eqtr4id ⊢ W ∈ CMod → * = * F