# Metamath Proof Explorer

## Theorem hdmapinvlem2

Description: Line 28 in Baer p. 110, 0 = f(w,u). (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 hdmapinvlem2 ( 𝜑 → ( ( 𝑆𝐶 ) ‘ 𝐸 ) = 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 1 2 3 4 5 6 7 8 9 10 11 12 hdmapinvlem1 ( 𝜑 → ( ( 𝑆𝐸 ) ‘ 𝐶 ) = 0 )
14 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
16 eqid ( 0g𝑈 ) = ( 0g𝑈 )
17 1 14 15 4 5 16 2 11 dvheveccl ( 𝜑𝐸 ∈ ( 𝑉 ∖ { ( 0g𝑈 ) } ) )
18 17 eldifad ( 𝜑𝐸𝑉 )
19 18 snssd ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
20 1 4 5 3 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
21 11 19 20 syl2anc ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
22 21 12 sseldd ( 𝜑𝐶𝑉 )
23 1 4 5 6 9 10 11 18 22 hdmapip0com ( 𝜑 → ( ( ( 𝑆𝐸 ) ‘ 𝐶 ) = 0 ↔ ( ( 𝑆𝐶 ) ‘ 𝐸 ) = 0 ) )
24 13 23 mpbid ( 𝜑 → ( ( 𝑆𝐶 ) ‘ 𝐸 ) = 0 )