mapdvalc

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

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		mapdvalc.c	$⊢ C = \{g \in F \| O (O (L (g))) = L (g)\}$
11	1 2 3 4 5 6 7 8 9	mapdval	$⊢ φ \to M (T) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\}$
12		anass	$⊢ ((f \in F \land O (O (L (f))) = L (f)) \land O (L (f)) \subseteq T) \leftrightarrow (f \in F \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T))$
13	10	lcfl1lem	$⊢ f \in C \leftrightarrow (f \in F \land O (O (L (f))) = L (f))$
14	13	anbi1i	$⊢ (f \in C \land O (L (f)) \subseteq T) \leftrightarrow ((f \in F \land O (O (L (f))) = L (f)) \land O (L (f)) \subseteq T)$
15	14	bicomi	$⊢ ((f \in F \land O (O (L (f))) = L (f)) \land O (L (f)) \subseteq T) \leftrightarrow (f \in C \land O (L (f)) \subseteq T)$
16	15	a1i	$⊢ φ \to (((f \in F \land O (O (L (f))) = L (f)) \land O (L (f)) \subseteq T) \leftrightarrow (f \in C \land O (L (f)) \subseteq T))$
17	12 16	bitr3id	$⊢ φ \to ((f \in F \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)) \leftrightarrow (f \in C \land O (L (f)) \subseteq T))$
18	17	rabbidva2	$⊢ φ \to \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq T)\} = \{f \in C \| O (L (f)) \subseteq T\}$
19	11 18	eqtrd	$⊢ φ \to M (T) = \{f \in C \| O (L (f)) \subseteq T\}$

Metamath Proof Explorer