# 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 ${⊢}{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 hdmapinvlem1

### 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 eqid ${⊢}\mathrm{LFnl}\left({U}\right)=\mathrm{LFnl}\left({U}\right)$
14 eqid ${⊢}\mathrm{LKer}\left({U}\right)=\mathrm{LKer}\left({U}\right)$
15 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
16 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
17 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
18 1 15 16 4 5 17 2 11 dvheveccl ${⊢}{\phi }\to {E}\in \left({V}\setminus \left\{{0}_{{U}}\right\}\right)$
19 18 eldifad ${⊢}{\phi }\to {E}\in {V}$
20 1 3 4 5 13 14 10 11 19 hdmaplkr ${⊢}{\phi }\to \mathrm{LKer}\left({U}\right)\left({S}\left({E}\right)\right)={O}\left(\left\{{E}\right\}\right)$
21 12 20 eleqtrrd ${⊢}{\phi }\to {C}\in \mathrm{LKer}\left({U}\right)\left({S}\left({E}\right)\right)$
22 1 4 11 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
23 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
24 eqid ${⊢}{\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
25 1 4 5 23 24 10 11 19 hdmapcl ${⊢}{\phi }\to {S}\left({E}\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
26 1 23 24 4 13 11 25 lcdvbaselfl ${⊢}{\phi }\to {S}\left({E}\right)\in \mathrm{LFnl}\left({U}\right)$
27 19 snssd ${⊢}{\phi }\to \left\{{E}\right\}\subseteq {V}$
28 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}$
29 11 27 28 syl2anc ${⊢}{\phi }\to {O}\left(\left\{{E}\right\}\right)\subseteq {V}$
30 29 12 sseldd ${⊢}{\phi }\to {C}\in {V}$
31 5 6 9 13 14 22 26 30 ellkr2
32 21 31 mpbid