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=\mathrm{LHyp}\left(K\right)$$
	hdmap12b.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmap12b.v	$$⊢V={\mathrm{Base}}_U$$
	hdmap12b.m	$$⊢M={inv}_g\left(U\right)$$
	hdmap12b.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hdmap12b.i	$$⊢I={inv}_g\left(C\right)$$
	hdmap12b.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmap12b.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmap12b.x	$$⊢\phi \to T\in V$$
Assertion	hdmapneg	$$⊢\phi \to S\left(M\left(T\right)\right)=I\left(S\left(T\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmap12b.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmap12b.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmap12b.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmap12b.m	$$⊢M={inv}_g\left(U\right)$$
5		hdmap12b.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hdmap12b.i	$$⊢I={inv}_g\left(C\right)$$
7		hdmap12b.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
8		hdmap12b.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
9		hdmap12b.x	$$⊢\phi \to T\in V$$
10	1 5 8	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
11		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
12	1 2 3 5 11 7 8 9	hdmapcl	$$⊢\phi \to S\left(T\right)\in {\mathrm{Base}}_C$$
13		eqid	$$⊢{+}_C={+}_C$$
14		eqid	$$⊢0_C=0_C$$
15	11 13 14 6	lmodvnegid	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(T\right)\in {\mathrm{Base}}_C\right)\to S\left(T\right){+}_{C}I\left(S\left(T\right)\right)=0_C$$
16	10 12 15	syl2anc	$$⊢\phi \to S\left(T\right){+}_{C}I\left(S\left(T\right)\right)=0_C$$
17	1 2 8	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
18		eqid	$$⊢{+}_U={+}_U$$
19		eqid	$$⊢0_U=0_U$$
20	3 18 19 4	lmodvnegid	$$⊢\left(U\in \mathrm{LMod}\wedge T\in V\right)\to T{+}_{U}M\left(T\right)=0_U$$
21	17 9 20	syl2anc	$$⊢\phi \to T{+}_{U}M\left(T\right)=0_U$$
22	3 4	lmodvnegcl	$$⊢\left(U\in \mathrm{LMod}\wedge T\in V\right)\to M\left(T\right)\in V$$
23	17 9 22	syl2anc	$$⊢\phi \to M\left(T\right)\in V$$
24	3 18	lmodvacl	$$⊢\left(U\in \mathrm{LMod}\wedge T\in V\wedge M\left(T\right)\in V\right)\to T{+}_{U}M\left(T\right)\in V$$
25	17 9 23 24	syl3anc	$$⊢\phi \to T{+}_{U}M\left(T\right)\in V$$
26	1 2 3 19 5 14 7 8 25	hdmapeq0	$$⊢\phi \to \left(S\left(T{+}_{U}M\left(T\right)\right)=0_C\leftrightarrow T{+}_{U}M\left(T\right)=0_U\right)$$
27	21 26	mpbird	$$⊢\phi \to S\left(T{+}_{U}M\left(T\right)\right)=0_C$$
28	1 2 3 18 5 13 7 8 9 23	hdmapadd	$$⊢\phi \to S\left(T{+}_{U}M\left(T\right)\right)=S\left(T\right){+}_{C}S\left(M\left(T\right)\right)$$
29	16 27 28	3eqtr2rd	$$⊢\phi \to S\left(T\right){+}_{C}S\left(M\left(T\right)\right)=S\left(T\right){+}_{C}I\left(S\left(T\right)\right)$$
30	1 2 3 5 11 7 8 23	hdmapcl	$$⊢\phi \to S\left(M\left(T\right)\right)\in {\mathrm{Base}}_C$$
31	11 6	lmodvnegcl	$$⊢\left(C\in \mathrm{LMod}\wedge S\left(T\right)\in {\mathrm{Base}}_C\right)\to I\left(S\left(T\right)\right)\in {\mathrm{Base}}_C$$
32	10 12 31	syl2anc	$$⊢\phi \to I\left(S\left(T\right)\right)\in {\mathrm{Base}}_C$$
33	11 13	lmodlcan	$$⊢\left(C\in \mathrm{LMod}\wedge \left(S\left(M\left(T\right)\right)\in {\mathrm{Base}}_C\wedge I\left(S\left(T\right)\right)\in {\mathrm{Base}}_C\wedge S\left(T\right)\in {\mathrm{Base}}_C\right)\right)\to \left(S\left(T\right){+}_{C}S\left(M\left(T\right)\right)=S\left(T\right){+}_{C}I\left(S\left(T\right)\right)\leftrightarrow S\left(M\left(T\right)\right)=I\left(S\left(T\right)\right)\right)$$
34	10 30 32 12 33	syl13anc	$$⊢\phi \to \left(S\left(T\right){+}_{C}S\left(M\left(T\right)\right)=S\left(T\right){+}_{C}I\left(S\left(T\right)\right)\leftrightarrow S\left(M\left(T\right)\right)=I\left(S\left(T\right)\right)\right)$$
35	29 34	mpbid	$$⊢\phi \to S\left(M\left(T\right)\right)=I\left(S\left(T\right)\right)$$