mapdcv

Description: Covering property of the converse of the map defined by df-mapd . (Contributed by NM, 14-Mar-2015)

	Ref	Expression
Hypotheses	mapdcv.h	$⊢ H = LHyp (K)$
	mapdcv.m	$⊢ M = mapd (K) (W)$
	mapdcv.u	$⊢ U = DVecH (K) (W)$
	mapdcv.s	$⊢ S = LSubSp (U)$
	mapdcv.c	$⊢ C = ⋖_{L} (U)$
	mapdcv.d	$⊢ D = LCDual (K) (W)$
	mapdcv.e	$⊢ E = ⋖_{L} (D)$
	mapdcv.k	$⊢ φ \to (K \in HL \land W \in H)$
	mapdcv.x	$⊢ φ \to X \in S$
	mapdcv.y	$⊢ φ \to Y \in S$
Assertion	mapdcv	$⊢ φ \to (X C Y \leftrightarrow M (X) E M (Y))$

Proof

Step	Hyp	Ref	Expression
1		mapdcv.h	$⊢ H = LHyp (K)$
2		mapdcv.m	$⊢ M = mapd (K) (W)$
3		mapdcv.u	$⊢ U = DVecH (K) (W)$
4		mapdcv.s	$⊢ S = LSubSp (U)$
5		mapdcv.c	$⊢ C = ⋖_{L} (U)$
6		mapdcv.d	$⊢ D = LCDual (K) (W)$
7		mapdcv.e	$⊢ E = ⋖_{L} (D)$
8		mapdcv.k	$⊢ φ \to (K \in HL \land W \in H)$
9		mapdcv.x	$⊢ φ \to X \in S$
10		mapdcv.y	$⊢ φ \to Y \in S$
11	1 2 3 4 8 9 10	mapdsord	$⊢ φ \to (M (X) \subset M (Y) \leftrightarrow X \subset Y)$
12		eqid	$⊢ LSubSp (D) = LSubSp (D)$
13	8	adantr	$⊢ (φ \land v \in S) \to (K \in HL \land W \in H)$
14		simpr	$⊢ (φ \land v \in S) \to v \in S$
15	1 2 3 4 6 12 13 14	mapdcl2	$⊢ (φ \land v \in S) \to M (v) \in LSubSp (D)$
16	8	adantr	$⊢ (φ \land f \in LSubSp (D)) \to (K \in HL \land W \in H)$
17	1 2 6 12 8	mapdrn2	$⊢ φ \to ran M = LSubSp (D)$
18	17	eleq2d	$⊢ φ \to (f \in ran M \leftrightarrow f \in LSubSp (D))$
19	18	biimpar	$⊢ (φ \land f \in LSubSp (D)) \to f \in ran M$
20	1 2 3 4 16 19	mapdcnvcl	$⊢ (φ \land f \in LSubSp (D)) \to M^{-1} (f) \in S$
21	1 2 16 19	mapdcnvid2	$⊢ (φ \land f \in LSubSp (D)) \to M (M^{-1} (f)) = f$
22	21	eqcomd	$⊢ (φ \land f \in LSubSp (D)) \to f = M (M^{-1} (f))$
23		fveq2	$⊢ v = M^{-1} (f) \to M (v) = M (M^{-1} (f))$
24	23	rspceeqv	$⊢ (M^{-1} (f) \in S \land f = M (M^{-1} (f))) \to \exists v \in S f = M (v)$
25	20 22 24	syl2anc	$⊢ (φ \land f \in LSubSp (D)) \to \exists v \in S f = M (v)$
26		psseq2	$⊢ f = M (v) \to (M (X) \subset f \leftrightarrow M (X) \subset M (v))$
27		psseq1	$⊢ f = M (v) \to (f \subset M (Y) \leftrightarrow M (v) \subset M (Y))$
28	26 27	anbi12d	$⊢ f = M (v) \to ((M (X) \subset f \land f \subset M (Y)) \leftrightarrow (M (X) \subset M (v) \land M (v) \subset M (Y)))$
29	28	adantl	$⊢ (φ \land f = M (v)) \to ((M (X) \subset f \land f \subset M (Y)) \leftrightarrow (M (X) \subset M (v) \land M (v) \subset M (Y)))$
30	15 25 29	rexxfrd	$⊢ φ \to (\exists f \in LSubSp (D) (M (X) \subset f \land f \subset M (Y)) \leftrightarrow \exists v \in S (M (X) \subset M (v) \land M (v) \subset M (Y)))$
31	9	adantr	$⊢ (φ \land v \in S) \to X \in S$
32	1 2 3 4 13 31 14	mapdsord	$⊢ (φ \land v \in S) \to (M (X) \subset M (v) \leftrightarrow X \subset v)$
33	10	adantr	$⊢ (φ \land v \in S) \to Y \in S$
34	1 2 3 4 13 14 33	mapdsord	$⊢ (φ \land v \in S) \to (M (v) \subset M (Y) \leftrightarrow v \subset Y)$
35	32 34	anbi12d	$⊢ (φ \land v \in S) \to ((M (X) \subset M (v) \land M (v) \subset M (Y)) \leftrightarrow (X \subset v \land v \subset Y))$
36	35	rexbidva	$⊢ φ \to (\exists v \in S (M (X) \subset M (v) \land M (v) \subset M (Y)) \leftrightarrow \exists v \in S (X \subset v \land v \subset Y))$
37	30 36	bitrd	$⊢ φ \to (\exists f \in LSubSp (D) (M (X) \subset f \land f \subset M (Y)) \leftrightarrow \exists v \in S (X \subset v \land v \subset Y))$
38	37	notbid	$⊢ φ \to (\neg \exists f \in LSubSp (D) (M (X) \subset f \land f \subset M (Y)) \leftrightarrow \neg \exists v \in S (X \subset v \land v \subset Y))$
39	11 38	anbi12d	$⊢ φ \to ((M (X) \subset M (Y) \land \neg \exists f \in LSubSp (D) (M (X) \subset f \land f \subset M (Y))) \leftrightarrow (X \subset Y \land \neg \exists v \in S (X \subset v \land v \subset Y)))$
40	1 6 8	lcdlmod	$⊢ φ \to D \in LMod$
41	1 2 3 4 6 12 8 9	mapdcl2	$⊢ φ \to M (X) \in LSubSp (D)$
42	1 2 3 4 6 12 8 10	mapdcl2	$⊢ φ \to M (Y) \in LSubSp (D)$
43	12 7 40 41 42	lcvbr	$⊢ φ \to (M (X) E M (Y) \leftrightarrow (M (X) \subset M (Y) \land \neg \exists f \in LSubSp (D) (M (X) \subset f \land f \subset M (Y))))$
44	1 3 8	dvhlmod	$⊢ φ \to U \in LMod$
45	4 5 44 9 10	lcvbr	$⊢ φ \to (X C Y \leftrightarrow (X \subset Y \land \neg \exists v \in S (X \subset v \land v \subset Y)))$
46	39 43 45	3bitr4rd	$⊢ φ \to (X C Y \leftrightarrow M (X) E M (Y))$

Metamath Proof Explorer

Theorem mapdcv

Proof