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 ) )