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