# 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 ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hdmapinvlem1.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
hdmapinvlem1.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
hdmapinvlem1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hdmapinvlem1.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
hdmapinvlem1.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hdmapinvlem1.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
hdmapinvlem1.t
hdmapinvlem1.z
hdmapinvlem1.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
hdmapinvlem1.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
hdmapinvlem1.c ${⊢}{\phi }\to {C}\in {O}\left(\left\{{E}\right\}\right)$
Assertion hdmapinvlem2

### Proof

Step Hyp Ref Expression
1 hdmapinvlem1.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hdmapinvlem1.e ${⊢}{E}=⟨{\mathrm{I}↾}_{{\mathrm{Base}}_{{K}}},{\mathrm{I}↾}_{\mathrm{LTrn}\left({K}\right)\left({W}\right)}⟩$
3 hdmapinvlem1.o ${⊢}{O}=\mathrm{ocH}\left({K}\right)\left({W}\right)$
4 hdmapinvlem1.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
5 hdmapinvlem1.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
6 hdmapinvlem1.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
7 hdmapinvlem1.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
8 hdmapinvlem1.t
9 hdmapinvlem1.z
10 hdmapinvlem1.s ${⊢}{S}=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
11 hdmapinvlem1.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
12 hdmapinvlem1.c ${⊢}{\phi }\to {C}\in {O}\left(\left\{{E}\right\}\right)$
13 1 2 3 4 5 6 7 8 9 10 11 12 hdmapinvlem1
14 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
15 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
16 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
17 1 14 15 4 5 16 2 11 dvheveccl ${⊢}{\phi }\to {E}\in \left({V}\setminus \left\{{0}_{{U}}\right\}\right)$
18 17 eldifad ${⊢}{\phi }\to {E}\in {V}$
19 18 snssd ${⊢}{\phi }\to \left\{{E}\right\}\subseteq {V}$
20 1 4 5 3 dochssv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left\{{E}\right\}\subseteq {V}\right)\to {O}\left(\left\{{E}\right\}\right)\subseteq {V}$
21 11 19 20 syl2anc ${⊢}{\phi }\to {O}\left(\left\{{E}\right\}\right)\subseteq {V}$
22 21 12 sseldd ${⊢}{\phi }\to {C}\in {V}$
23 1 4 5 6 9 10 11 18 22 hdmapip0com
24 13 23 mpbid