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

Metamath Proof Explorer

Theorem clmnegneg

Description: Double negative of a vector. (Contributed by NM, 6-Aug-2007) (Revised by AV, 21-Sep-2021)

Ref Expression
Hypotheses clmpm1dir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmpm1dir.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmpm1dir.a ⊢ + = ( +g ‘ 𝑊 )
Assertion clmnegneg ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( - 1 · ( - 1 · 𝐴 ) ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 clmpm1dir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmpm1dir.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 clmpm1dir.a ⊢ + = ( +g ‘ 𝑊 )
4 neg1mulneg1e1 ⊢ ( - 1 · - 1 ) = 1
5 4 oveq1i ⊢ ( ( - 1 · - 1 ) · 𝐴 ) = ( 1 · 𝐴 )
6 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
9 7 8 clmneg1 ⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
10 9 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
11 simpr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
12 1 7 2 8 clmvsass ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ 𝑉 ) ) → ( ( - 1 · - 1 ) · 𝐴 ) = ( - 1 · ( - 1 · 𝐴 ) ) )
13 6 10 10 11 12 syl13anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( ( - 1 · - 1 ) · 𝐴 ) = ( - 1 · ( - 1 · 𝐴 ) ) )
14 1 2 clmvs1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 1 · 𝐴 ) = 𝐴 )
15 5 13 14 3eqtr3a ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( - 1 · ( - 1 · 𝐴 ) ) = 𝐴 )