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	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	hdmapf1oN	$⊢ φ \to S : V \underset{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	$⊢ φ \to (K \in HL \land W \in H)$
8	1 2 3 6 7	hdmapfnN	$⊢ φ \to S Fn V$
9	1 4 5 6 7	hdmaprnN	$⊢ φ \to ran S = D$
10	7	adantr	$⊢ (φ \land (x \in V \land y \in V)) \to (K \in HL \land W \in H)$
11		simprl	$⊢ (φ \land (x \in V \land y \in V)) \to x \in V$
12		simprr	$⊢ (φ \land (x \in V \land y \in V)) \to y \in V$
13	1 2 3 6 10 11 12	hdmap11	$⊢ (φ \land (x \in V \land y \in V)) \to (S (x) = S (y) \leftrightarrow x = y)$
14	13	biimpd	$⊢ (φ \land (x \in V \land y \in V)) \to (S (x) = S (y) \to x = y)$
15	14	ralrimivva	$⊢ φ \to \forall x \in V \forall y \in V (S (x) = S (y) \to x = y)$
16		dff1o6	$⊢ S : V \underset{1-1 onto}{⟶} D \leftrightarrow (S Fn V \land ran S = D \land \forall x \in V \forall y \in V (S (x) = S (y) \to x = y))$
17	8 9 15 16	syl3anbrc	$⊢ φ \to S : V \underset{1-1 onto}{⟶} D$

Metamath Proof Explorer

Theorem hdmapf1oN

Proof