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 · 𝐴 ) ) = 𝐴 )