mapdsn

Description: Value of the map defined by df-mapd at the span of a singleton. (Contributed by NM, 16-Feb-2015)

	Ref	Expression
Hypotheses	mapdsn.h	$⊢ H = LHyp (K)$
	mapdsn.o	$⊢ O = ocH (K) (W)$
	mapdsn.m	$⊢ M = mapd (K) (W)$
	mapdsn.u	$⊢ U = DVecH (K) (W)$
	mapdsn.v	$⊢ V = {Base}_{U}$
	mapdsn.n	$⊢ N = LSpan (U)$
	mapdsn.f	$⊢ F = LFnl (U)$
	mapdsn.l	$⊢ L = LKer (U)$
	mapdsn.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdsn.x	$⊢ φ \to X \in V$
Assertion	mapdsn	$⊢ φ \to M (N (\{X\})) = \{f \in F \| O (\{X\}) \subseteq L (f)\}$

Proof

Step	Hyp	Ref	Expression
1		mapdsn.h	$⊢ H = LHyp (K)$
2		mapdsn.o	$⊢ O = ocH (K) (W)$
3		mapdsn.m	$⊢ M = mapd (K) (W)$
4		mapdsn.u	$⊢ U = DVecH (K) (W)$
5		mapdsn.v	$⊢ V = {Base}_{U}$
6		mapdsn.n	$⊢ N = LSpan (U)$
7		mapdsn.f	$⊢ F = LFnl (U)$
8		mapdsn.l	$⊢ L = LKer (U)$
9		mapdsn.k	$⊢ φ \to (K \in HL \land W \in H)$
10		mapdsn.x	$⊢ φ \to X \in V$
11		eqid	$⊢ LSubSp (U) = LSubSp (U)$
12	1 4 9	dvhlmod	$⊢ φ \to U \in LMod$
13	5 11 6	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
14	12 10 13	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
15	1 4 11 7 8 2 3 9 14	mapdval	$⊢ φ \to M (N (\{X\})) = \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))\}$
16	9	ad2antrr	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to (K \in HL \land W \in H)$
17	10	snssd	$⊢ φ \to \{X\} \subseteq V$
18	5 6	lspssv	$⊢ (U \in LMod \land \{X\} \subseteq V) \to N (\{X\}) \subseteq V$
19	12 17 18	syl2anc	$⊢ φ \to N (\{X\}) \subseteq V$
20	19	ad2antrr	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to N (\{X\}) \subseteq V$
21		simprr	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to O (L (f)) \subseteq N (\{X\})$
22	1 4 5 2	dochss	$⊢ ((K \in HL \land W \in H) \land N (\{X\}) \subseteq V \land O (L (f)) \subseteq N (\{X\})) \to O (N (\{X\})) \subseteq O (O (L (f)))$
23	16 20 21 22	syl3anc	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to O (N (\{X\})) \subseteq O (O (L (f)))$
24	1 4 2 5 6 9 17	dochocsp	$⊢ φ \to O (N (\{X\})) = O (\{X\})$
25	24	ad2antrr	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to O (N (\{X\})) = O (\{X\})$
26		simprl	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to O (O (L (f))) = L (f)$
27	23 25 26	3sstr3d	$⊢ ((φ \land f \in F) \land (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))) \to O (\{X\}) \subseteq L (f)$
28	9	ad2antrr	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to (K \in HL \land W \in H)$
29		simplr	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to f \in F$
30	10	ad2antrr	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to X \in V$
31		simpr	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to O (\{X\}) \subseteq L (f)$
32	1 2 4 5 7 8 28 29 30 31	lcfl9a	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to O (O (L (f))) = L (f)$
33	12	ad2antrr	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to U \in LMod$
34	5 7 8 33 29	lkrssv	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to L (f) \subseteq V$
35	1 4 5 2	dochss	$⊢ ((K \in HL \land W \in H) \land L (f) \subseteq V \land O (\{X\}) \subseteq L (f)) \to O (L (f)) \subseteq O (O (\{X\}))$
36	28 34 31 35	syl3anc	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to O (L (f)) \subseteq O (O (\{X\}))$
37	1 4 2 5 6 9 10	dochocsn	$⊢ φ \to O (O (\{X\})) = N (\{X\})$
38	37	ad2antrr	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to O (O (\{X\})) = N (\{X\})$
39	36 38	sseqtrd	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to O (L (f)) \subseteq N (\{X\})$
40	32 39	jca	$⊢ ((φ \land f \in F) \land O (\{X\}) \subseteq L (f)) \to (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))$
41	27 40	impbida	$⊢ (φ \land f \in F) \to ((O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\})) \leftrightarrow O (\{X\}) \subseteq L (f))$
42	41	rabbidva	$⊢ φ \to \{f \in F \| (O (O (L (f))) = L (f) \land O (L (f)) \subseteq N (\{X\}))\} = \{f \in F \| O (\{X\}) \subseteq L (f)\}$
43	15 42	eqtrd	$⊢ φ \to M (N (\{X\})) = \{f \in F \| O (\{X\}) \subseteq L (f)\}$

Metamath Proof Explorer

Theorem mapdsn

Proof