# Metamath Proof Explorer

## Theorem hgmapval0

Description: Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hgmapval0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hgmapval0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hgmapval0.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hgmapval0.o
hgmapval0.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
hgmapval0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hgmapval0

### Proof

Step Hyp Ref Expression
1 hgmapval0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hgmapval0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hgmapval0.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
4 hgmapval0.o
5 hgmapval0.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
6 hgmapval0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
8 eqid ${⊢}{0}_{{U}}={0}_{{U}}$
9 1 2 7 8 6 dvh1dim ${⊢}{\phi }\to \exists {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}{x}\ne {0}_{{U}}$
10 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
11 eqid ${⊢}{0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
12 eqid ${⊢}\mathrm{HDMap}\left({K}\right)\left({W}\right)=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
13 6 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
14 simpr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to {x}\in {\mathrm{Base}}_{{U}}$
15 1 2 7 8 10 11 12 13 14 hdmapeq0 ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \left(\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}↔{x}={0}_{{U}}\right)$
16 15 biimpd ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \left(\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\to {x}={0}_{{U}}\right)$
17 16 necon3ad ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \left({x}\ne {0}_{{U}}\to ¬\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\right)$
18 17 3impia ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\wedge {x}\ne {0}_{{U}}\right)\to ¬\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
19 1 2 6 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
20 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
21 7 3 20 4 8 lmod0vs
22 19 21 sylan
23 22 fveq2d
24 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
25 eqid ${⊢}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
26 3 24 4 lmod0cl
27 19 26 syl
29 1 2 7 20 3 24 10 25 12 5 13 14 28 hgmapvs
30 1 2 8 10 11 12 6 hdmapval0 ${⊢}{\phi }\to \mathrm{HDMap}\left({K}\right)\left({W}\right)\left({0}_{{U}}\right)={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
31 30 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \mathrm{HDMap}\left({K}\right)\left({W}\right)\left({0}_{{U}}\right)={0}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
32 23 29 31 3eqtr3d
33 eqid ${⊢}{\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
34 eqid ${⊢}\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)=\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)$
35 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)}$
36 eqid ${⊢}{0}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)}={0}_{\mathrm{Scalar}\left(\mathrm{LCDual}\left({K}\right)\left({W}\right)\right)}$
37 1 10 6 lcdlvec ${⊢}{\phi }\to \mathrm{LCDual}\left({K}\right)\left({W}\right)\in \mathrm{LVec}$
38 37 adantr ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \mathrm{LCDual}\left({K}\right)\left({W}\right)\in \mathrm{LVec}$
39 1 2 13 dvhlmod ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to {U}\in \mathrm{LMod}$
40 39 26 syl
41 1 2 3 24 10 34 35 5 13 40 hgmapdcl
42 1 2 7 10 33 12 13 14 hdmapcl ${⊢}\left({\phi }\wedge {x}\in {\mathrm{Base}}_{{U}}\right)\to \mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
43 33 25 34 35 36 11 38 41 42 lvecvs0or
44 32 43 mpbid
45 44 orcomd
46 45 ord