Metamath Proof Explorer

Theorem hdmapfnN

Description: Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	hdmapfn.h	$⊢ H = LHyp (K)$
		hdmapfn.u	$⊢ U = DVecH (K) (W)$
		hdmapfn.v	$⊢ V = {Base}_{U}$
		hdmapfn.s	$⊢ S = HDMap (K) (W)$
		hdmapfn.k	$⊢ φ \to (K \in HL \land W \in H)$
	Assertion	hdmapfnN	$⊢ φ \to S Fn V$

Proof

Step	Hyp	Ref	Expression
1		hdmapfn.h	$⊢ H = LHyp (K)$
2		hdmapfn.u	$⊢ U = DVecH (K) (W)$
3		hdmapfn.v	$⊢ V = {Base}_{U}$
4		hdmapfn.s	$⊢ S = HDMap (K) (W)$
5		hdmapfn.k	$⊢ φ \to (K \in HL \land W \in H)$
6		riotaex	$⊢ (ι y \in {Base}_{LCDual (K) (W)} \| \forall z \in V (\neg z \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{t\})) \to y = HDMap1 (K) (W) (⟨z, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), z⟩), t⟩))) \in V$
7		eqid	$⊢ (t \in V ⟼ (ι y \in {Base}_{LCDual (K) (W)} \| \forall z \in V (\neg z \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{t\})) \to y = HDMap1 (K) (W) (⟨z, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), z⟩), t⟩)))) = (t \in V ⟼ (ι y \in {Base}_{LCDual (K) (W)} \| \forall z \in V (\neg z \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{t\})) \to y = HDMap1 (K) (W) (⟨z, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), z⟩), t⟩))))$
8	6 7	fnmpti	$⊢ (t \in V ⟼ (ι y \in {Base}_{LCDual (K) (W)} \| \forall z \in V (\neg z \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{t\})) \to y = HDMap1 (K) (W) (⟨z, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), z⟩), t⟩)))) Fn 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	$⊢ LCDual (K) (W) = LCDual (K) (W)$
12		eqid	$⊢ {Base}_{LCDual (K) (W)} = {Base}_{LCDual (K) (W)}$
13		eqid	$⊢ HVMap (K) (W) = HVMap (K) (W)$
14		eqid	$⊢ HDMap1 (K) (W) = HDMap1 (K) (W)$
15	1 9 2 3 10 11 12 13 14 4 5	hdmapfval	$⊢ φ \to S = (t \in V ⟼ (ι y \in {Base}_{LCDual (K) (W)} \| \forall z \in V (\neg z \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{t\})) \to y = HDMap1 (K) (W) (⟨z, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), z⟩), t⟩))))$
16	15	fneq1d	$⊢ φ \to (S Fn V \leftrightarrow (t \in V ⟼ (ι y \in {Base}_{LCDual (K) (W)} \| \forall z \in V (\neg z \in (LSpan (U) (\{⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩\}) \cup LSpan (U) (\{t\})) \to y = HDMap1 (K) (W) (⟨z, HDMap1 (K) (W) (⟨⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩, HVMap (K) (W) (⟨{I ↾}_{{Base}_{K}}, {I ↾}_{LTrn (K) (W)}⟩), z⟩), t⟩)))) Fn V)$
17	8 16	mpbiri	$⊢ φ \to S Fn V$