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 ⊢ 𝐹 = ( 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 ∈ 𝐾 )