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 
|- V = ( Base ` W )
clmpm1dir.s 
|- .x. = ( .s ` W )
clmpm1dir.a 
|- .+ = ( +g ` W )
Assertion clmnegneg 
|- ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. ( -u 1 .x. A ) ) = A )

Proof

Step Hyp Ref Expression
1 clmpm1dir.v 
 |-  V = ( Base ` W )
2 clmpm1dir.s 
 |-  .x. = ( .s ` W )
3 clmpm1dir.a 
 |-  .+ = ( +g ` W )
4 neg1mulneg1e1 
 |-  ( -u 1 x. -u 1 ) = 1
5 4 oveq1i 
 |-  ( ( -u 1 x. -u 1 ) .x. A ) = ( 1 .x. A )
6 simpl 
 |-  ( ( W e. CMod /\ A e. V ) -> W e. CMod )
7 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
8 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
9 7 8 clmneg1 
 |-  ( W e. CMod -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
10 9 adantr 
 |-  ( ( W e. CMod /\ A e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
11 simpr 
 |-  ( ( W e. CMod /\ A e. V ) -> A e. V )
12 1 7 2 8 clmvsass 
 |-  ( ( W e. CMod /\ ( -u 1 e. ( Base ` ( Scalar ` W ) ) /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ A e. V ) ) -> ( ( -u 1 x. -u 1 ) .x. A ) = ( -u 1 .x. ( -u 1 .x. A ) ) )
13 6 10 10 11 12 syl13anc 
 |-  ( ( W e. CMod /\ A e. V ) -> ( ( -u 1 x. -u 1 ) .x. A ) = ( -u 1 .x. ( -u 1 .x. A ) ) )
14 1 2 clmvs1 
 |-  ( ( W e. CMod /\ A e. V ) -> ( 1 .x. A ) = A )
15 5 13 14 3eqtr3a 
 |-  ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. ( -u 1 .x. A ) ) = A )