Metamath Proof Explorer

Theorem clmvz

Description: Two ways to express the negative of a vector. (Contributed by NM, 29-Feb-2008) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvz.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmvz.m ⊢ − = ( -g ‘ 𝑊 )
clmvz.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmvz.0 ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion clmvz ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 0 − 𝐴 ) = ( - 1 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 clmvz.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmvz.m ⊢ − = ( -g ‘ 𝑊 )
3 clmvz.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 clmvz.0 ⊢ 0 = ( 0g ‘ 𝑊 )
5 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
6 clmgrp ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ Grp )
7 1 4 grpidcl ⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝑉 )
8 6 7 syl ⊢ ( 𝑊 ∈ ℂMod → 0 ∈ 𝑉 )
9 8 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 0 ∈ 𝑉 )
10 simpr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
11 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
12 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13 1 11 2 12 3 clmvsubval2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 0 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 0 − 𝐴 ) = ( ( - 1 · 𝐴 ) ( +g ‘ 𝑊 ) 0 ) )
14 5 9 10 13 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 0 − 𝐴 ) = ( ( - 1 · 𝐴 ) ( +g ‘ 𝑊 ) 0 ) )
15 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
16 12 15 clmneg1 ⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
17 16 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
18 1 12 3 15 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ 𝑉 ) → ( - 1 · 𝐴 ) ∈ 𝑉 )
19 5 17 10 18 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( - 1 · 𝐴 ) ∈ 𝑉 )
20 1 11 4 grprid ⊢ ( ( 𝑊 ∈ Grp ∧ ( - 1 · 𝐴 ) ∈ 𝑉 ) → ( ( - 1 · 𝐴 ) ( +g ‘ 𝑊 ) 0 ) = ( - 1 · 𝐴 ) )
21 6 19 20 syl2an2r ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( ( - 1 · 𝐴 ) ( +g ‘ 𝑊 ) 0 ) = ( - 1 · 𝐴 ) )
22 14 21 eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ) → ( 0 − 𝐴 ) = ( - 1 · 𝐴 ) )