# 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 = ( LHyp ` K )`
hgmapeq0.u
`|- U = ( ( DVecH ` K ) ` W )`
hgmapeq0.r
`|- R = ( Scalar ` U )`
hgmapeq0.b
`|- B = ( Base ` R )`
hgmapeq0.o
`|- .0. = ( 0g ` R )`
hgmapeq0.g
`|- G = ( ( HGMap ` K ) ` W )`
hgmapeq0.k
`|- ( ph -> ( K e. HL /\ W e. H ) )`
hgmapeq0.x
`|- ( ph -> X e. B )`
Assertion hgmapeq0
`|- ( ph -> ( ( G ` X ) = .0. <-> X = .0. ) )`

### Proof

Step Hyp Ref Expression
1 hgmapeq0.h
` |-  H = ( LHyp ` K )`
2 hgmapeq0.u
` |-  U = ( ( DVecH ` K ) ` W )`
3 hgmapeq0.r
` |-  R = ( Scalar ` U )`
4 hgmapeq0.b
` |-  B = ( Base ` R )`
5 hgmapeq0.o
` |-  .0. = ( 0g ` R )`
6 hgmapeq0.g
` |-  G = ( ( HGMap ` K ) ` W )`
7 hgmapeq0.k
` |-  ( ph -> ( K e. HL /\ W e. H ) )`
8 hgmapeq0.x
` |-  ( ph -> X e. B )`
9 1 2 3 5 6 7 hgmapval0
` |-  ( ph -> ( G ` .0. ) = .0. )`
10 9 eqeq2d
` |-  ( ph -> ( ( G ` X ) = ( G ` .0. ) <-> ( G ` X ) = .0. ) )`
11 1 2 7 dvhlmod
` |-  ( ph -> U e. LMod )`
12 3 4 5 lmod0cl
` |-  ( U e. LMod -> .0. e. B )`
13 11 12 syl
` |-  ( ph -> .0. e. B )`
14 1 2 3 4 6 7 8 13 hgmap11
` |-  ( ph -> ( ( G ` X ) = ( G ` .0. ) <-> X = .0. ) )`
15 10 14 bitr3d
` |-  ( ph -> ( ( G ` X ) = .0. <-> X = .0. ) )`