Theorem hdmapf1oN

Description: Part 12 in Baer p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd , this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hdmapf1o.h	|- H = ( LHyp ` K )
	hdmapf1o.u	|- U = ( ( DVecH ` K ) ` W )
	hdmapf1o.v	|- V = ( Base ` U )
	hdmapf1o.c	|- C = ( ( LCDual ` K ) ` W )
	hdmapf1o.d	|- D = ( Base ` C )
	hdmapf1o.s	|- S = ( ( HDMap ` K ) ` W )
	hdmapf1o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion	hdmapf1oN	|- ( ph -> S : V -1-1-onto-> D )

Proof

Step	Hyp	Ref	Expression
1		hdmapf1o.h	|- H = ( LHyp ` K )
2		hdmapf1o.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmapf1o.v	|- V = ( Base ` U )
4		hdmapf1o.c	|- C = ( ( LCDual ` K ) ` W )
5		hdmapf1o.d	|- D = ( Base ` C )
6		hdmapf1o.s	|- S = ( ( HDMap ` K ) ` W )
7		hdmapf1o.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8	1 2 3 6 7	hdmapfnN	|- ( ph -> S Fn V )
9	1 4 5 6 7	hdmaprnN	|- ( ph -> ran S = D )
10	7	adantr	|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( K e. HL /\ W e. H ) )
11		simprl	|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> x e. V )
12		simprr	|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> y e. V )
13	1 2 3 6 10 11 12	hdmap11	|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( ( S ` x ) = ( S ` y ) <-> x = y ) )
14	13	biimpd	|- ( ( ph /\ ( x e. V /\ y e. V ) ) -> ( ( S ` x ) = ( S ` y ) -> x = y ) )
15	14	ralrimivva	|- ( ph -> A. x e. V A. y e. V ( ( S ` x ) = ( S ` y ) -> x = y ) )
16		dff1o6	|- ( S : V -1-1-onto-> D <-> ( S Fn V /\ ran S = D /\ A. x e. V A. y e. V ( ( S ` x ) = ( S ` y ) -> x = y ) ) )
17	8 9 15 16	syl3anbrc	|- ( ph -> S : V -1-1-onto-> D )