This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ CMod → − 1 ∈ K

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ F = Scalar ⁡ W
2 clmsub.k ⊢ K = Base F
3 1 2 clmzss ⊢ W ∈ CMod → ℤ ⊆ K
4 neg1z ⊢ − 1 ∈ ℤ
5 ssel ⊢ ℤ ⊆ K → − 1 ∈ ℤ → − 1 ∈ K
6 3 4 5 mpisyl ⊢ W ∈ CMod → − 1 ∈ K