# Metamath Proof Explorer

## Theorem hgmapeq0

Description: The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015)

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

### Proof

Step Hyp Ref Expression
1 hgmapeq0.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hgmapeq0.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hgmapeq0.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
4 hgmapeq0.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
5 hgmapeq0.o
6 hgmapeq0.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
7 hgmapeq0.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
8 hgmapeq0.x ${⊢}{\phi }\to {X}\in {B}$
9 1 2 3 5 6 7 hgmapval0
10 9 eqeq2d
11 1 2 7 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
12 3 4 5 lmod0cl
13 11 12 syl
14 1 2 3 4 6 7 8 13 hgmap11
15 10 14 bitr3d