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 ⊢ F = Scalar ⁡ W
clmsub.k ⊢ K = Base F
Assertion clmneg ⊢ W ∈ CMod ∧ A ∈ K → − A = inv g ⁡ 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 → inv g ⁡ F = inv g ⁡ ℂ fld ↾ 𝑠 K
5 4 adantr ⊢ W ∈ CMod ∧ A ∈ K → inv g ⁡ F = inv g ⁡ ℂ fld ↾ 𝑠 K
6 5 fveq1d ⊢ W ∈ CMod ∧ A ∈ K → inv g ⁡ F ⁡ A = inv g ⁡ ℂ 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 eqid ⊢ inv g ⁡ ℂ fld = inv g ⁡ ℂ fld
12 eqid ⊢ inv g ⁡ ℂ fld ↾ 𝑠 K = inv g ⁡ ℂ fld ↾ 𝑠 K
13 10 11 12 subginv ⊢ K ∈ SubGrp ⁡ ℂ fld ∧ A ∈ K → inv g ⁡ ℂ fld ⁡ A = inv g ⁡ ℂ fld ↾ 𝑠 K ⁡ A
14 9 13 sylan ⊢ W ∈ CMod ∧ A ∈ K → inv g ⁡ ℂ fld ⁡ A = inv g ⁡ ℂ fld ↾ 𝑠 K ⁡ A
15 1 2 clmsscn ⊢ W ∈ CMod → K ⊆ ℂ
16 15 sselda ⊢ W ∈ CMod ∧ A ∈ K → A ∈ ℂ
17 cnfldneg ⊢ A ∈ ℂ → inv g ⁡ ℂ fld ⁡ A = − A
18 16 17 syl ⊢ W ∈ CMod ∧ A ∈ K → inv g ⁡ ℂ fld ⁡ A = − A
19 6 14 18 3eqtr2rd ⊢ W ∈ CMod ∧ A ∈ K → − A = inv g ⁡ F ⁡ A