Theorem hdmapinvlem1

Description: Line 27 in Baer p. 110. We use C for Baer's u. Our unit vector E has the required properties for his w by hdmapevec2 . Our ( ( SE )C ) means the inner product <. C , E >. i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015)

	Ref	Expression
Hypotheses	hdmapinvlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapinvlem1.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
	hdmapinvlem1.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapinvlem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapinvlem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmapinvlem1.t	⊢ · = ( .r ‘ 𝑅 )
	hdmapinvlem1.z	⊢ 0 = ( 0g ‘ 𝑅 )
	hdmapinvlem1.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapinvlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapinvlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
Assertion	hdmapinvlem1	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		hdmapinvlem1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapinvlem1.e	⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3		hdmapinvlem1.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapinvlem1.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		hdmapinvlem1.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		hdmapinvlem1.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
7		hdmapinvlem1.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
8		hdmapinvlem1.t	⊢ · = ( .r ‘ 𝑅 )
9		hdmapinvlem1.z	⊢ 0 = ( 0g ‘ 𝑅 )
10		hdmapinvlem1.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
11		hdmapinvlem1.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		hdmapinvlem1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
13		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
14		eqid	⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
15		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
16		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
17		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
18	1 15 16 4 5 17 2 11	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
19	18	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
20	1 3 4 5 13 14 10 11 19	hdmaplkr	⊢ ( 𝜑 → ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝐸 ) ) = ( 𝑂 ‘ { 𝐸 } ) )
21	12 20	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝐸 ) ) )
22	1 4 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
23		eqid	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
24		eqid	⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
25	1 4 5 23 24 10 11 19	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
26	1 23 24 4 13 11 25	lcdvbaselfl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝐸 ) ∈ ( LFnl ‘ 𝑈 ) )
27	19	snssd	⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
28	1 4 5 3	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
29	11 27 28	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
30	29 12	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
31	5 6 9 13 14 22 26 30	ellkr2	⊢ ( 𝜑 → ( 𝐶 ∈ ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝐸 ) ) ↔ ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) = 0 ) )
32	21 31	mpbid	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐶 ) = 0 )