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

Metamath Proof Explorer

Theorem clmvneg1

Description: Minus 1 times a vector is the negative of the vector. Equation 2 of Kreyszig p. 51. ( lmodvneg1 analog.) (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clmvneg1.v 
|- V = ( Base ` W )
clmvneg1.n 
|- N = ( invg ` W )
clmvneg1.f 
|- F = ( Scalar ` W )
clmvneg1.s 
|- .x. = ( .s ` W )
Assertion clmvneg1 
|- ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( N ` X ) )

Proof

Step Hyp Ref Expression
1 clmvneg1.v 
 |-  V = ( Base ` W )
2 clmvneg1.n 
 |-  N = ( invg ` W )
3 clmvneg1.f 
 |-  F = ( Scalar ` W )
4 clmvneg1.s 
 |-  .x. = ( .s ` W )
5 eqid 
 |-  ( Base ` F ) = ( Base ` F )
6 3 5 clmzss 
 |-  ( W e. CMod -> ZZ C_ ( Base ` F ) )
7 1zzd 
 |-  ( W e. CMod -> 1 e. ZZ )
8 6 7 sseldd 
 |-  ( W e. CMod -> 1 e. ( Base ` F ) )
9 3 5 clmneg 
 |-  ( ( W e. CMod /\ 1 e. ( Base ` F ) ) -> -u 1 = ( ( invg ` F ) ` 1 ) )
10 8 9 mpdan 
 |-  ( W e. CMod -> -u 1 = ( ( invg ` F ) ` 1 ) )
11 3 clm1 
 |-  ( W e. CMod -> 1 = ( 1r ` F ) )
12 11 fveq2d 
 |-  ( W e. CMod -> ( ( invg ` F ) ` 1 ) = ( ( invg ` F ) ` ( 1r ` F ) ) )
13 10 12 eqtrd 
 |-  ( W e. CMod -> -u 1 = ( ( invg ` F ) ` ( 1r ` F ) ) )
14 13 adantr 
 |-  ( ( W e. CMod /\ X e. V ) -> -u 1 = ( ( invg ` F ) ` ( 1r ` F ) ) )
15 14 oveq1d 
 |-  ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. X ) )
16 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
17 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
18 eqid 
 |-  ( invg ` F ) = ( invg ` F )
19 1 2 3 4 17 18 lmodvneg1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. X ) = ( N ` X ) )
20 16 19 sylan 
 |-  ( ( W e. CMod /\ X e. V ) -> ( ( ( invg ` F ) ` ( 1r ` F ) ) .x. X ) = ( N ` X ) )
21 15 20 eqtrd 
 |-  ( ( W e. CMod /\ X e. V ) -> ( -u 1 .x. X ) = ( N ` X ) )