Theorem clmsub

Description: Subtraction 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	clmsub	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	clmsubrg	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4		subrgsubg	⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
5	3 4	syl	⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
6		cnfldsub	⊢ − = ( -g ‘ ℂfld )
7		eqid	⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
8		eqid	⊢ ( -g ‘ ( ℂfld ↾s 𝐾 ) ) = ( -g ‘ ( ℂfld ↾s 𝐾 ) )
9	6 7 8	subgsub	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
10	5 9	syl3an1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
11	1 2	clmsca	⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
12	11	fveq2d	⊢ ( 𝑊 ∈ ℂMod → ( -g ‘ 𝐹 ) = ( -g ‘ ( ℂfld ↾s 𝐾 ) ) )
13	12	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( -g ‘ 𝐹 ) = ( -g ‘ ( ℂfld ↾s 𝐾 ) ) )
14	13	oveqd	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 𝐴 ( -g ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
15	10 14	eqtr4d	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) )