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 = ( LHyp ` K )
	hgmapf1o.u	|- U = ( ( DVecH ` K ) ` W )
	hgmapf1o.r	|- R = ( Scalar ` U )
	hgmapf1o.b	|- B = ( Base ` R )
	hgmapf1o.g	|- G = ( ( HGMap ` K ) ` W )
	hgmapf1o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	hgmapf1oN	|- ( ph -> G : B -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		hgmapf1o.h	|- H = ( LHyp ` K )
2		hgmapf1o.u	|- U = ( ( DVecH ` K ) ` W )
3		hgmapf1o.r	|- R = ( Scalar ` U )
4		hgmapf1o.b	|- B = ( Base ` R )
5		hgmapf1o.g	|- G = ( ( HGMap ` K ) ` W )
6		hgmapf1o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
7	1 2 3 4 5 6	hgmapfnN	|- ( ph -> G Fn B )
8	1 2 3 4 5 6	hgmaprnN	|- ( ph -> ran G = B )
9	6	adantr	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( K e. HL /\ W e. H ) )
10		simprl	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
11		simprr	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
12	1 2 3 4 5 9 10 11	hgmap11	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( G ` x ) = ( G ` y ) <-> x = y ) )
13	12	biimpd	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( G ` x ) = ( G ` y ) -> x = y ) )
14	13	ralrimivva	|- ( ph -> A. x e. B A. y e. B ( ( G ` x ) = ( G ` y ) -> x = y ) )
15		dff1o6	|- ( G : B -1-1-onto-> B <-> ( G Fn B /\ ran G = B /\ A. x e. B A. y e. B ( ( G ` x ) = ( G ` y ) -> x = y ) ) )
16	7 8 14 15	syl3anbrc	|- ( ph -> G : B -1-1-onto-> B )