mapdval

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 27-Jan-2015)

	Ref	Expression
Hypotheses	mapdval.h	$⊢ H = LHyp (K)$
	mapdval.u	$⊢ U = DVecH (K) (W)$
	mapdval.s	$⊢ S = LSubSp (U)$
	mapdval.f	$⊢ F = LFnl (U)$
	mapdval.l	$⊢ L = LKer (U)$
	mapdval.o	$⊢ O = ocH (K) (W)$
	mapdval.m	$⊢ M = mapd (K) (W)$
	mapdval.k	$⊢ φ \to (K \in X \land W \in H)$
	mapdval.t	$⊢ φ \to T \in S$
Assertion	mapdval	$⊢ φ \to M (T) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\}$

Proof

Step	Hyp	Ref	Expression
1		mapdval.h	$⊢ H = LHyp (K)$
2		mapdval.u	$⊢ U = DVecH (K) (W)$
3		mapdval.s	$⊢ S = LSubSp (U)$
4		mapdval.f	$⊢ F = LFnl (U)$
5		mapdval.l	$⊢ L = LKer (U)$
6		mapdval.o	$⊢ O = ocH (K) (W)$
7		mapdval.m	$⊢ M = mapd (K) (W)$
8		mapdval.k	$⊢ φ \to (K \in X \land W \in H)$
9		mapdval.t	$⊢ φ \to T \in S$
10	1 2 3 4 5 6 7	mapdfval	$⊢ (K \in X \land W \in H) \to M = (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\})$
11	8 10	syl	$⊢ φ \to M = (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\})$
12	11	fveq1d	$⊢ φ \to M (T) = (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\}) (T)$
13	4	fvexi	$⊢ F \in V$
14	13	rabex	$⊢ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\} \in V$
15		sseq2	$⊢ s = T \to (O (L (f)) \subseteq s \leftrightarrow O (L (f)) \subseteq T)$
16	15	anbi2d	$⊢ s = T \to ((O (O (L (f))) = L (f) \land O (L (f)) \subseteq s) \leftrightarrow (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T))$
17	16	rabbidv	$⊢ s = T \to \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\} = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\}$
18		eqid	$⊢ (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\}) = (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\})$
19	17 18	fvmptg	$⊢ (T \in S \land \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\} \in V) \to (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\}) (T) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\}$
20	9 14 19	sylancl	$⊢ φ \to (s \in S ⟼ \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq s)\}) (T) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\}$
21	12 20	eqtrd	$⊢ φ \to M (T) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\}$

Metamath Proof Explorer

Theorem mapdval

Proof