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 )