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

Metamath Proof Explorer

Theorem clmneg

Description: Negation 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 clmneg ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → - 𝐴 = ( ( invg ‘ 𝐹 ) ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 1 2 clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
4 3 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( invg ‘ 𝐹 ) = ( invg ‘ ( ℂfld ↾s 𝐾 ) ) )
5 4 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( invg ‘ 𝐹 ) = ( invg ‘ ( ℂfld ↾s 𝐾 ) ) )
6 5 fveq1d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( invg ‘ 𝐹 ) ‘ 𝐴 ) = ( ( invg ‘ ( ℂ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 eqid ⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
12 eqid ⊢ ( invg ‘ ( ℂfld ↾s 𝐾 ) ) = ( invg ‘ ( ℂfld ↾s 𝐾 ) )
13 10 11 12 subginv ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = ( ( invg ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) )
14 9 13 sylan ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = ( ( invg ‘ ( ℂfld ↾s 𝐾 ) ) ‘ 𝐴 ) )
15 1 2 clmsscn ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
16 15 sselda ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → 𝐴 ∈ ℂ )
17 cnfldneg ⊢ ( 𝐴 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
18 16 17 syl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → ( ( invg ‘ ℂfld ) ‘ 𝐴 ) = - 𝐴 )
19 6 14 18 3eqtr2rd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ) → - 𝐴 = ( ( invg ‘ 𝐹 ) ‘ 𝐴 ) )