Theorem clmneg1

Description: Minus one is in the scalar ring of a subcomplex module. (Contributed by AV, 28-Sep-2021)

	Ref	Expression
Hypotheses	clm0.f	|- F = ( Scalar ` W )
	clmsub.k	|- K = ( Base ` F )
Assertion	clmneg1	|- ( W e. CMod -> -u 1 e. K )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	|- F = ( Scalar ` W )
2		clmsub.k	|- K = ( Base ` F )
3	1 2	clmzss	|- ( W e. CMod -> ZZ C_ K )
4		neg1z	|- -u 1 e. ZZ
5		ssel	|- ( ZZ C_ K -> ( -u 1 e. ZZ -> -u 1 e. K ) )
6	3 4 5	mpisyl	|- ( W e. CMod -> -u 1 e. K )