hdmapcl

Description: Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmapcl.h	$⊢ H = LHyp (K)$
	hdmapcl.u	$⊢ U = DVecH (K) (W)$
	hdmapcl.v	$⊢ V = {Base}_{U}$
	hdmapcl.c	$⊢ C = LCDual (K) (W)$
	hdmapcl.d	$⊢ D = {Base}_{C}$
	hdmapcl.s	$⊢ S = HDMap (K) (W)$
	hdmapcl.k	$⊢ φ \to (K \in HL \land W \in H)$
	hdmapcl.t	$⊢ φ \to T \in V$
Assertion	hdmapcl	$⊢ φ \to S (T) \in D$

Proof

Step	Hyp	Ref	Expression
1		hdmapcl.h	$⊢ H = LHyp (K)$
2		hdmapcl.u	$⊢ U = DVecH (K) (W)$
3		hdmapcl.v	$⊢ V = {Base}_{U}$
4		hdmapcl.c	$⊢ C = LCDual (K) (W)$
5		hdmapcl.d	$⊢ D = {Base}_{C}$
6		hdmapcl.s	$⊢ S = HDMap (K) (W)$
7		hdmapcl.k	$⊢ φ \to (K \in HL \land W \in H)$
8		hdmapcl.t	$⊢ φ \to T \in V$
9		eqid	$⊢ ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ = ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩$
10		eqid	$⊢ LSpan (U) = LSpan (U)$
11		eqid	$⊢ HVMap (K) (W) = HVMap (K) (W)$
12		eqid	$⊢ HDMap1 (K) (W) = HDMap1 (K) (W)$
13	1 9 2 3 10 4 5 11 12 6 7 8	hdmapval	$⊢ φ \to S (T) = (ι h \in D \| \forall y \in V (\neg y \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{T\})) \to h = HDMap1 (K) (W) (⟨y, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), y⟩), T⟩)))$
14		eqid	$⊢ 0_{U} = 0_{U}$
15		eqid	$⊢ LSpan (C) = LSpan (C)$
16		eqid	$⊢ mapd (K) (W) = mapd (K) (W)$
17		eqid	$⊢ {Base}_{K} = {Base}_{K}$
18		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
19	1 17 18 2 3 14 9 7	dvheveccl	$⊢ φ \to ⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩ \in (V ∖ \{0_{U}\})$
20	1 2 3 14 10 4 15 16 11 7 19	mapdhvmap	$⊢ φ \to mapd (K) (W) (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\})) = LSpan (C) (\{HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩)\})$
21		eqid	$⊢ 0_{C} = 0_{C}$
22	1 2 3 14 4 5 21 11 7 19	hvmapcl2	$⊢ φ \to HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩) \in (D ∖ \{0_{C}\})$
23	22	eldifad	$⊢ φ \to HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩) \in D$
24	1 2 3 14 10 4 5 15 16 12 7 20 19 23 8	hdmap1eu	$⊢ φ \to \exists! h \in D \forall y \in V (\neg y \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{T\})) \to h = HDMap1 (K) (W) (⟨y, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), y⟩), T⟩))$
25		riotacl	$⊢ \exists! h \in D \forall y \in V (\neg y \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{T\})) \to h = HDMap1 (K) (W) (⟨y, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), y⟩), T⟩)) \to (ι h \in D \| \forall y \in V (\neg y \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{T\})) \to h = HDMap1 (K) (W) (⟨y, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), y⟩), T⟩))) \in D$
26	24 25	syl	$⊢ φ \to (ι h \in D \| \forall y \in V (\neg y \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{T\})) \to h = HDMap1 (K) (W) (⟨y, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), y⟩), T⟩))) \in D$
27	13 26	eqeltrd	$⊢ φ \to S (T) \in D$

Metamath Proof Explorer

Theorem hdmapcl

Proof