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 ‘ 𝐹 ) ‘ 𝐴 ) )