Theorem clmsubcl

Description: Closure of ring subtraction for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmsubcl	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 − 𝑌 ) ∈ 𝐾 )

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	6	subgsubcl	⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 − 𝑌 ) ∈ 𝐾 )
8	5 7	syl3an1	⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐾 ) → ( 𝑋 − 𝑌 ) ∈ 𝐾 )