mapdspex

Description: The map of a span equals the dual span of some vector (functional). (Contributed by NM, 15-Mar-2015)

	Ref	Expression
Hypotheses	mapdspex.h	$⊢ H = LHyp (K)$
	mapdspex.m	$⊢ M = mapd (K) (W)$
	mapdspex.u	$⊢ U = DVecH (K) (W)$
	mapdspex.v	$⊢ V = {Base}_{U}$
	mapdspex.n	$⊢ N = LSpan (U)$
	mapdspex.c	$⊢ C = LCDual (K) (W)$
	mapdspex.b	$⊢ B = {Base}_{C}$
	mapdspex.j	$⊢ J = LSpan (C)$
	mapdspex.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdspex.x	$⊢ φ \to X \in V$
Assertion	mapdspex	$⊢ φ \to \exists g \in B M (N (\{X\})) = J (\{g\})$

Proof

Step	Hyp	Ref	Expression
1		mapdspex.h	$⊢ H = LHyp (K)$
2		mapdspex.m	$⊢ M = mapd (K) (W)$
3		mapdspex.u	$⊢ U = DVecH (K) (W)$
4		mapdspex.v	$⊢ V = {Base}_{U}$
5		mapdspex.n	$⊢ N = LSpan (U)$
6		mapdspex.c	$⊢ C = LCDual (K) (W)$
7		mapdspex.b	$⊢ B = {Base}_{C}$
8		mapdspex.j	$⊢ J = LSpan (C)$
9		mapdspex.k	$⊢ φ \to (K \in HL \land W \in H)$
10		mapdspex.x	$⊢ φ \to X \in V$
11	1 6 9	lcdlmod	$⊢ φ \to C \in LMod$
12	11	adantr	$⊢ (φ \land N (\{X\}) \in LSAtoms (U)) \to C \in LMod$
13		eqid	$⊢ LSAtoms (U) = LSAtoms (U)$
14		eqid	$⊢ LSAtoms (C) = LSAtoms (C)$
15	9	adantr	$⊢ (φ \land N (\{X\}) \in LSAtoms (U)) \to (K \in HL \land W \in H)$
16		simpr	$⊢ (φ \land N (\{X\}) \in LSAtoms (U)) \to N (\{X\}) \in LSAtoms (U)$
17	1 2 3 13 6 14 15 16	mapdat	$⊢ (φ \land N (\{X\}) \in LSAtoms (U)) \to M (N (\{X\})) \in LSAtoms (C)$
18	7 8 14	islsati	$⊢ (C \in LMod \land M (N (\{X\})) \in LSAtoms (C)) \to \exists g \in B M (N (\{X\})) = J (\{g\})$
19	12 17 18	syl2anc	$⊢ (φ \land N (\{X\}) \in LSAtoms (U)) \to \exists g \in B M (N (\{X\})) = J (\{g\})$
20		eqid	$⊢ 0_{C} = 0_{C}$
21	1 6 7 20 9	lcd0vcl	$⊢ φ \to 0_{C} \in B$
22	21	adantr	$⊢ (φ \land N (\{X\}) = \{0_{U}\}) \to 0_{C} \in B$
23		fveq2	$⊢ N (\{X\}) = \{0_{U}\} \to M (N (\{X\})) = M (\{0_{U}\})$
24		eqid	$⊢ 0_{U} = 0_{U}$
25	1 2 3 24 6 20 9	mapd0	$⊢ φ \to M (\{0_{U}\}) = \{0_{C}\}$
26	20 8	lspsn0	$⊢ C \in LMod \to J (\{0_{C}\}) = \{0_{C}\}$
27	11 26	syl	$⊢ φ \to J (\{0_{C}\}) = \{0_{C}\}$
28	25 27	eqtr4d	$⊢ φ \to M (\{0_{U}\}) = J (\{0_{C}\})$
29	23 28	sylan9eqr	$⊢ (φ \land N (\{X\}) = \{0_{U}\}) \to M (N (\{X\})) = J (\{0_{C}\})$
30		sneq	$⊢ g = 0_{C} \to \{g\} = \{0_{C}\}$
31	30	fveq2d	$⊢ g = 0_{C} \to J (\{g\}) = J (\{0_{C}\})$
32	31	rspceeqv	$⊢ (0_{C} \in B \land M (N (\{X\})) = J (\{0_{C}\})) \to \exists g \in B M (N (\{X\})) = J (\{g\})$
33	22 29 32	syl2anc	$⊢ (φ \land N (\{X\}) = \{0_{U}\}) \to \exists g \in B M (N (\{X\})) = J (\{g\})$
34	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
35	4 5 24 13 34 10	lsator0sp	$⊢ φ \to (N (\{X\}) \in LSAtoms (U) \lor N (\{X\}) = \{0_{U}\})$
36	19 33 35	mpjaodan	$⊢ φ \to \exists g \in B M (N (\{X\})) = J (\{g\})$

Metamath Proof Explorer

Theorem mapdspex

Proof