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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	clmneg1	⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		clm0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		clmsub.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
3	1 2	clmzss	⊢ ( 𝑊 ∈ ℂMod → ℤ ⊆ 𝐾 )
4		neg1z	⊢ - 1 ∈ ℤ
5		ssel	⊢ ( ℤ ⊆ 𝐾 → ( - 1 ∈ ℤ → - 1 ∈ 𝐾 ) )
6	3 4 5	mpisyl	⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ 𝐾 )