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 = inv g U
hdmap12b.c C = LCDual K W
hdmap12b.i I = inv g C
hdmap12b.s S = HDMap K W
hdmap12b.k φ K HL W H
hdmap12b.x φ T V
Assertion hdmapneg φ 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 = inv g U
5 hdmap12b.c C = LCDual K W
6 hdmap12b.i I = inv g C
7 hdmap12b.s S = HDMap K W
8 hdmap12b.k φ K HL W H
9 hdmap12b.x φ T V
10 1 5 8 lcdlmod φ C LMod
11 eqid Base C = Base C
12 1 2 3 5 11 7 8 9 hdmapcl φ S T Base C
13 eqid + C = + C
14 eqid 0 C = 0 C
15 11 13 14 6 lmodvnegid C LMod S T Base C S T + C I S T = 0 C
16 10 12 15 syl2anc φ S T + C I S T = 0 C
17 1 2 8 dvhlmod φ U LMod
18 eqid + U = + U
19 eqid 0 U = 0 U
20 3 18 19 4 lmodvnegid U LMod T V T + U M T = 0 U
21 17 9 20 syl2anc φ T + U M T = 0 U
22 3 4 lmodvnegcl U LMod T V M T V
23 17 9 22 syl2anc φ M T V
24 3 18 lmodvacl U LMod T V M T V T + U M T V
25 17 9 23 24 syl3anc φ T + U M T V
26 1 2 3 19 5 14 7 8 25 hdmapeq0 φ S T + U M T = 0 C T + U M T = 0 U
27 21 26 mpbird φ S T + U M T = 0 C
28 1 2 3 18 5 13 7 8 9 23 hdmapadd φ S T + U M T = S T + C S M T
29 16 27 28 3eqtr2rd φ S T + C S M T = S T + C I S T
30 1 2 3 5 11 7 8 23 hdmapcl φ S M T Base C
31 11 6 lmodvnegcl C LMod S T Base C I S T Base C
32 10 12 31 syl2anc φ I S T Base C
33 11 13 lmodlcan C LMod S M T Base C I S T Base C S T Base C S T + C S M T = S T + C I S T S M T = I S T
34 10 30 32 12 33 syl13anc φ S T + C S M T = S T + C I S T S M T = I S T
35 29 34 mpbid φ S M T = I S T