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=BaseF
Assertion clmneg ⊢W∈CMod∧A∈K→−A=invg⁡F⁡A

Proof

Step Hyp Ref Expression
1 clm0.f ⊢F=Scalar⁡W
2 clmsub.k ⊢K=BaseF
3 1 2 clmsca ⊢W∈CMod→F=ℂfld↾𝑠K
4 3 fveq2d ⊢W∈CMod→invg⁡F=invg⁡ℂfld↾𝑠K
5 4 adantr ⊢W∈CMod∧A∈K→invg⁡F=invg⁡ℂfld↾𝑠K
6 5 fveq1d ⊢W∈CMod∧A∈K→invg⁡F⁡A=invg⁡ℂ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 ⊢invg⁡ℂfld=invg⁡ℂfld
12 eqid ⊢invg⁡ℂfld↾𝑠K=invg⁡ℂfld↾𝑠K
13 10 11 12 subginv ⊢K∈SubGrp⁡ℂfld∧A∈K→invg⁡ℂfld⁡A=invg⁡ℂfld↾𝑠K⁡A
14 9 13 sylan ⊢W∈CMod∧A∈K→invg⁡ℂfld⁡A=invg⁡ℂfld↾𝑠K⁡A
15 1 2 clmsscn ⊢W∈CMod→K⊆ℂ
16 15 sselda ⊢W∈CMod∧A∈K→A∈ℂ
17 cnfldneg ⊢A∈ℂ→invg⁡ℂfld⁡A=−A
18 16 17 syl ⊢W∈CMod∧A∈K→invg⁡ℂfld⁡A=−A
19 6 14 18 3eqtr2rd ⊢W∈CMod∧A∈K→−A=invg⁡F⁡A