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

Metamath Proof Explorer

Theorem hdmapneg

Proof