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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmap12b.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmap12b.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmap12b.m	⊢ 𝑀 = ( invg ‘ 𝑈 )
	hdmap12b.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	hdmap12b.i	⊢ 𝐼 = ( invg ‘ 𝐶 )
	hdmap12b.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmap12b.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmap12b.x	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion	hdmapneg	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmap12b.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmap12b.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmap12b.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmap12b.m	⊢ 𝑀 = ( invg ‘ 𝑈 )
5		hdmap12b.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6		hdmap12b.i	⊢ 𝐼 = ( invg ‘ 𝐶 )
7		hdmap12b.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8		hdmap12b.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		hdmap12b.x	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
10	1 5 8	lcdlmod	⊢ ( 𝜑 → 𝐶 ∈ LMod )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12	1 2 3 5 11 7 8 9	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑇 ) ∈ ( Base ‘ 𝐶 ) )
13		eqid	⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
14		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
15	11 13 14 6	lmodvnegid	⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑆 ‘ 𝑇 ) ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) = ( 0g ‘ 𝐶 ) )
16	10 12 15	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) = ( 0g ‘ 𝐶 ) )
17	1 2 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
18		eqid	⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
19		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
20	3 18 19 4	lmodvnegid	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ) → ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) = ( 0g ‘ 𝑈 ) )
21	17 9 20	syl2anc	⊢ ( 𝜑 → ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) = ( 0g ‘ 𝑈 ) )
22	3 4	lmodvnegcl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ) → ( 𝑀 ‘ 𝑇 ) ∈ 𝑉 )
23	17 9 22	syl2anc	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) ∈ 𝑉 )
24	3 18	lmodvacl	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑇 ∈ 𝑉 ∧ ( 𝑀 ‘ 𝑇 ) ∈ 𝑉 ) → ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) ∈ 𝑉 )
25	17 9 23 24	syl3anc	⊢ ( 𝜑 → ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) ∈ 𝑉 )
26	1 2 3 19 5 14 7 8 25	hdmapeq0	⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) ) = ( 0g ‘ 𝐶 ) ↔ ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) = ( 0g ‘ 𝑈 ) ) )
27	21 26	mpbird	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) ) = ( 0g ‘ 𝐶 ) )
28	1 2 3 18 5 13 7 8 9 23	hdmapadd	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑇 ( +g ‘ 𝑈 ) ( 𝑀 ‘ 𝑇 ) ) ) = ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) ) )
29	16 27 28	3eqtr2rd	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) ) = ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) )
30	1 2 3 5 11 7 8 23	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐶 ) )
31	11 6	lmodvnegcl	⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑆 ‘ 𝑇 ) ∈ ( Base ‘ 𝐶 ) ) → ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐶 ) )
32	10 12 31	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐶 ) )
33	11 13	lmodlcan	⊢ ( ( 𝐶 ∈ LMod ∧ ( ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑆 ‘ 𝑇 ) ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) ) = ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) ↔ ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) )
34	10 30 32 12 33	syl13anc	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) ) = ( ( 𝑆 ‘ 𝑇 ) ( +g ‘ 𝐶 ) ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) ↔ ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) ) )
35	29 34	mpbid	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑀 ‘ 𝑇 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ 𝑇 ) ) )