hvmapvalvalN

Description: Value of value of map (i.e. functional value) from nonzero vectors to nonzero functionals in the closed kernel dual space. (Contributed by NM, 23-Mar-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvmapval.h	$⊢ H = LHyp (K)$
	hvmapval.u	$⊢ U = DVecH (K) (W)$
	hvmapval.o	$⊢ O = ocH (K) (W)$
	hvmapval.v	$⊢ V = {Base}_{U}$
	hvmapval.p	$⊢ \underset{˙}{+} = +_{U}$
	hvmapval.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hvmapval.z	$⊢ \underset{˙}{0} = 0_{U}$
	hvmapval.s	$⊢ S = Scalar (U)$
	hvmapval.r	$⊢ R = {Base}_{S}$
	hvmapval.m	$⊢ M = HVMap (K) (W)$
	hvmapval.k	$⊢ φ \to (K \in A \land W \in H)$
	hvmapval.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	hvmapval.y	$⊢ φ \to Y \in V$
Assertion	hvmapvalvalN	$⊢ φ \to M (X) (Y) = (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$

Proof

Step	Hyp	Ref	Expression
1		hvmapval.h	$⊢ H = LHyp (K)$
2		hvmapval.u	$⊢ U = DVecH (K) (W)$
3		hvmapval.o	$⊢ O = ocH (K) (W)$
4		hvmapval.v	$⊢ V = {Base}_{U}$
5		hvmapval.p	$⊢ \underset{˙}{+} = +_{U}$
6		hvmapval.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
7		hvmapval.z	$⊢ \underset{˙}{0} = 0_{U}$
8		hvmapval.s	$⊢ S = Scalar (U)$
9		hvmapval.r	$⊢ R = {Base}_{S}$
10		hvmapval.m	$⊢ M = HVMap (K) (W)$
11		hvmapval.k	$⊢ φ \to (K \in A \land W \in H)$
12		hvmapval.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
13		hvmapval.y	$⊢ φ \to Y \in V$
14	1 2 3 4 5 6 7 8 9 10 11 12	hvmapval	$⊢ φ \to M (X) = (y \in V ⟼ (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X)))$
15	14	fveq1d	$⊢ φ \to M (X) (Y) = (y \in V ⟼ (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))) (Y)$
16		riotaex	$⊢ (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X)) \in V$
17		eqeq1	$⊢ y = Y \to (y = t \underset{˙}{+} (j \underset{˙}{\cdot} X) \leftrightarrow Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$
18	17	rexbidv	$⊢ y = Y \to (\exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X) \leftrightarrow \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$
19	18	riotabidv	$⊢ y = Y \to (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X)) = (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$
20		eqid	$⊢ (y \in V ⟼ (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))) = (y \in V ⟼ (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X)))$
21	19 20	fvmptg	$⊢ (Y \in V \land (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X)) \in V) \to (y \in V ⟼ (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))) (Y) = (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$
22	13 16 21	sylancl	$⊢ φ \to (y \in V ⟼ (ι j \in R \| \exists t \in O (\{X\}) y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))) (Y) = (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$
23	15 22	eqtrd	$⊢ φ \to M (X) (Y) = (ι j \in R \| \exists t \in O (\{X\}) Y = t \underset{˙}{+} (j \underset{˙}{\cdot} X))$

Metamath Proof Explorer

Theorem hvmapvalvalN

Proof