Theorem hgmapf1oN

Description: The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hgmapf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmapf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmapf1o.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmapf1o.b	$$⊢B={\mathrm{Base}}_R$$
	hgmapf1o.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmapf1o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	hgmapf1oN	$$⊢\phi \to G:B\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		hgmapf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmapf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmapf1o.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		hgmapf1o.b	$$⊢B={\mathrm{Base}}_R$$
5		hgmapf1o.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
6		hgmapf1o.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7	1 2 3 4 5 6	hgmapfnN	$$⊢\phi \to GFnB$$
8	1 2 3 4 5 6	hgmaprnN	$$⊢\phi \to \mathrm{ran}G=B$$
9	6	adantr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		simprl	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x\in B$$
11		simprr	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to y\in B$$
12	1 2 3 4 5 9 10 11	hgmap11	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(G\left(x\right)=G\left(y\right)\leftrightarrow x=y\right)$$
13	12	biimpd	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to \left(G\left(x\right)=G\left(y\right)\to x=y\right)$$
14	13	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in B\left(G\left(x\right)=G\left(y\right)\to x=y\right)$$
15		dff1o6	$$⊢G:B\underset{1-1\; onto}{⟶}B\leftrightarrow \left(GFnB\wedge \mathrm{ran}G=B\wedge \forall x\in B\forall y\in B\left(G\left(x\right)=G\left(y\right)\to x=y\right)\right)$$
16	7 8 14 15	syl3anbrc	$$⊢\phi \to G:B\underset{1-1\; onto}{⟶}B$$