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	$$⊢\underset{\dot{}}{0}=0_R$$
	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	$$⊢\phi \to \left(G\left(X\right)=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$

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	$$⊢\underset{\dot{}}{0}=0_R$$
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	$$⊢\phi \to G\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
10	9	eqeq2d	$$⊢\phi \to \left(G\left(X\right)=G\left(\underset{\dot{}}{0}\right)\leftrightarrow G\left(X\right)=\underset{\dot{}}{0}\right)$$
11	1 2 7	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
12	3 4 5	lmod0cl	$$⊢U\in \mathrm{LMod}\to \underset{\dot{}}{0}\in B$$
13	11 12	syl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$
14	1 2 3 4 6 7 8 13	hgmap11	$$⊢\phi \to \left(G\left(X\right)=G\left(\underset{\dot{}}{0}\right)\leftrightarrow X=\underset{\dot{}}{0}\right)$$
15	10 14	bitr3d	$$⊢\phi \to \left(G\left(X\right)=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$