# 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 𝐻 = ( LHyp ‘ 𝐾 )
hgmapeq0.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmapeq0.r 𝑅 = ( Scalar ‘ 𝑈 )
hgmapeq0.b 𝐵 = ( Base ‘ 𝑅 )
hgmapeq0.o 0 = ( 0g𝑅 )
hgmapeq0.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapeq0.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
hgmapeq0.x ( 𝜑𝑋𝐵 )
Assertion hgmapeq0 ( 𝜑 → ( ( 𝐺𝑋 ) = 0𝑋 = 0 ) )

### Proof

Step Hyp Ref Expression
1 hgmapeq0.h 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmapeq0.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmapeq0.r 𝑅 = ( Scalar ‘ 𝑈 )
4 hgmapeq0.b 𝐵 = ( Base ‘ 𝑅 )
5 hgmapeq0.o 0 = ( 0g𝑅 )
6 hgmapeq0.g 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
7 hgmapeq0.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
8 hgmapeq0.x ( 𝜑𝑋𝐵 )
9 1 2 3 5 6 7 hgmapval0 ( 𝜑 → ( 𝐺0 ) = 0 )
10 9 eqeq2d ( 𝜑 → ( ( 𝐺𝑋 ) = ( 𝐺0 ) ↔ ( 𝐺𝑋 ) = 0 ) )
11 1 2 7 dvhlmod ( 𝜑𝑈 ∈ LMod )
12 3 4 5 lmod0cl ( 𝑈 ∈ LMod → 0𝐵 )
13 11 12 syl ( 𝜑0𝐵 )
14 1 2 3 4 6 7 8 13 hgmap11 ( 𝜑 → ( ( 𝐺𝑋 ) = ( 𝐺0 ) ↔ 𝑋 = 0 ) )
15 10 14 bitr3d ( 𝜑 → ( ( 𝐺𝑋 ) = 0𝑋 = 0 ) )