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=\mathrm{Scalar}\left(W\right)$$
	clmsub.k	$$⊢K={\mathrm{Base}}_F$$
Assertion	clmneg1	$$⊢W\in \mathrm{CMod}\to -1\in K$$

Proof

Step	Hyp	Ref	Expression
1		clm0.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		clmsub.k	$$⊢K={\mathrm{Base}}_F$$
3	1 2	clmzss	$$⊢W\in \mathrm{CMod}\to \mathbb{Z}\subseteq K$$
4		neg1z	$$⊢-1\in \mathbb{Z}$$
5		ssel	$$⊢\mathbb{Z}\subseteq K\to \left(-1\in \mathbb{Z}\to -1\in K\right)$$
6	3 4 5	mpisyl	$$⊢W\in \mathrm{CMod}\to -1\in K$$