Metamath Proof Explorer

Theorem hdmapneg

Description: Part of proof of part 12 in Baer p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015)

Ref Expression
Hypotheses hdmap12b.h 
|- H = ( LHyp ` K )
hdmap12b.u 
|- U = ( ( DVecH ` K ) ` W )
hdmap12b.v 
|- V = ( Base ` U )
hdmap12b.m 
|- M = ( invg ` U )
hdmap12b.c 
|- C = ( ( LCDual ` K ) ` W )
hdmap12b.i 
|- I = ( invg ` C )
hdmap12b.s 
|- S = ( ( HDMap ` K ) ` W )
hdmap12b.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmap12b.x 
|- ( ph -> T e. V )
Assertion hdmapneg 
|- ( ph -> ( S ` ( M ` T ) ) = ( I ` ( S ` T ) ) )

Proof

Step Hyp Ref Expression
1 hdmap12b.h 
 |-  H = ( LHyp ` K )
2 hdmap12b.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmap12b.v 
 |-  V = ( Base ` U )
4 hdmap12b.m 
 |-  M = ( invg ` U )
5 hdmap12b.c 
 |-  C = ( ( LCDual ` K ) ` W )
6 hdmap12b.i 
 |-  I = ( invg ` C )
7 hdmap12b.s 
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmap12b.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmap12b.x 
 |-  ( ph -> T e. V )
10 1 5 8 lcdlmod 
 |-  ( ph -> C e. LMod )
11 eqid 
 |-  ( Base ` C ) = ( Base ` C )
12 1 2 3 5 11 7 8 9 hdmapcl 
 |-  ( ph -> ( S ` T ) e. ( Base ` C ) )
13 eqid 
 |-  ( +g ` C ) = ( +g ` C )
14 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
15 11 13 14 6 lmodvnegid 
 |-  ( ( C e. LMod /\ ( S ` T ) e. ( Base ` C ) ) -> ( ( S ` T ) ( +g ` C ) ( I ` ( S ` T ) ) ) = ( 0g ` C ) )
16 10 12 15 syl2anc 
 |-  ( ph -> ( ( S ` T ) ( +g ` C ) ( I ` ( S ` T ) ) ) = ( 0g ` C ) )
17 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
18 eqid 
 |-  ( +g ` U ) = ( +g ` U )
19 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
20 3 18 19 4 lmodvnegid 
 |-  ( ( U e. LMod /\ T e. V ) -> ( T ( +g ` U ) ( M ` T ) ) = ( 0g ` U ) )
21 17 9 20 syl2anc 
 |-  ( ph -> ( T ( +g ` U ) ( M ` T ) ) = ( 0g ` U ) )
22 3 4 lmodvnegcl 
 |-  ( ( U e. LMod /\ T e. V ) -> ( M ` T ) e. V )
23 17 9 22 syl2anc 
 |-  ( ph -> ( M ` T ) e. V )
24 3 18 lmodvacl 
 |-  ( ( U e. LMod /\ T e. V /\ ( M ` T ) e. V ) -> ( T ( +g ` U ) ( M ` T ) ) e. V )
25 17 9 23 24 syl3anc 
 |-  ( ph -> ( T ( +g ` U ) ( M ` T ) ) e. V )
26 1 2 3 19 5 14 7 8 25 hdmapeq0 
 |-  ( ph -> ( ( S ` ( T ( +g ` U ) ( M ` T ) ) ) = ( 0g ` C ) <-> ( T ( +g ` U ) ( M ` T ) ) = ( 0g ` U ) ) )
27 21 26 mpbird 
 |-  ( ph -> ( S ` ( T ( +g ` U ) ( M ` T ) ) ) = ( 0g ` C ) )
28 1 2 3 18 5 13 7 8 9 23 hdmapadd 
 |-  ( ph -> ( S ` ( T ( +g ` U ) ( M ` T ) ) ) = ( ( S ` T ) ( +g ` C ) ( S ` ( M ` T ) ) ) )
29 16 27 28 3eqtr2rd 
 |-  ( ph -> ( ( S ` T ) ( +g ` C ) ( S ` ( M ` T ) ) ) = ( ( S ` T ) ( +g ` C ) ( I ` ( S ` T ) ) ) )
30 1 2 3 5 11 7 8 23 hdmapcl 
 |-  ( ph -> ( S ` ( M ` T ) ) e. ( Base ` C ) )
31 11 6 lmodvnegcl 
 |-  ( ( C e. LMod /\ ( S ` T ) e. ( Base ` C ) ) -> ( I ` ( S ` T ) ) e. ( Base ` C ) )
32 10 12 31 syl2anc 
 |-  ( ph -> ( I ` ( S ` T ) ) e. ( Base ` C ) )
33 11 13 lmodlcan 
 |-  ( ( C e. LMod /\ ( ( S ` ( M ` T ) ) e. ( Base ` C ) /\ ( I ` ( S ` T ) ) e. ( Base ` C ) /\ ( S ` T ) e. ( Base ` C ) ) ) -> ( ( ( S ` T ) ( +g ` C ) ( S ` ( M ` T ) ) ) = ( ( S ` T ) ( +g ` C ) ( I ` ( S ` T ) ) ) <-> ( S ` ( M ` T ) ) = ( I ` ( S ` T ) ) ) )
34 10 30 32 12 33 syl13anc 
 |-  ( ph -> ( ( ( S ` T ) ( +g ` C ) ( S ` ( M ` T ) ) ) = ( ( S ` T ) ( +g ` C ) ( I ` ( S ` T ) ) ) <-> ( S ` ( M ` T ) ) = ( I ` ( S ` T ) ) ) )
35 29 34 mpbid 
 |-  ( ph -> ( S ` ( M ` T ) ) = ( I ` ( S ` T ) ) )