Theorem clmsubcl

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

	Ref	Expression
Hypotheses	clm0.f	|- F = ( Scalar ` W )
	clmsub.k	|- K = ( Base ` F )
Assertion	clmsubcl	|- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X - Y ) e. K )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	|- F = ( Scalar ` W )
2		clmsub.k	|- K = ( Base ` F )
3	1 2	clmsubrg	|- ( W e. CMod -> K e. ( SubRing ` CCfld ) )
4		subrgsubg	|- ( K e. ( SubRing ` CCfld ) -> K e. ( SubGrp ` CCfld ) )
5	3 4	syl	|- ( W e. CMod -> K e. ( SubGrp ` CCfld ) )
6		cnfldsub	|- - = ( -g ` CCfld )
7	6	subgsubcl	|- ( ( K e. ( SubGrp ` CCfld ) /\ X e. K /\ Y e. K ) -> ( X - Y ) e. K )
8	5 7	syl3an1	|- ( ( W e. CMod /\ X e. K /\ Y e. K ) -> ( X - Y ) e. K )