Metamath Proof Explorer

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 )