lcvfbr

Description: The covers relation for a left vector space (or a left module). (Contributed by NM, 7-Jan-2015)

	Ref	Expression
Hypotheses	lcvfbr.s	$⊢ S = LSubSp (W)$
	lcvfbr.c	$⊢ C = ⋖_{L} (W)$
	lcvfbr.w	$⊢ φ \to W \in X$
Assertion	lcvfbr	$⊢ φ \to C = \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\}$

Proof

Step	Hyp	Ref	Expression
1		lcvfbr.s	$⊢ S = LSubSp (W)$
2		lcvfbr.c	$⊢ C = ⋖_{L} (W)$
3		lcvfbr.w	$⊢ φ \to W \in X$
4		elex	$⊢ W \in X \to W \in V$
5		fveq2	$⊢ w = W \to LSubSp (w) = LSubSp (W)$
6	5 1	eqtr4di	$⊢ w = W \to LSubSp (w) = S$
7	6	eleq2d	$⊢ w = W \to (t \in LSubSp (w) \leftrightarrow t \in S)$
8	6	eleq2d	$⊢ w = W \to (u \in LSubSp (w) \leftrightarrow u \in S)$
9	7 8	anbi12d	$⊢ w = W \to ((t \in LSubSp (w) \land u \in LSubSp (w)) \leftrightarrow (t \in S \land u \in S))$
10	6	rexeqdv	$⊢ w = W \to (\exists s \in LSubSp (w) (t \subset s \land s \subset u) \leftrightarrow \exists s \in S (t \subset s \land s \subset u))$
11	10	notbid	$⊢ w = W \to (\neg \exists s \in LSubSp (w) (t \subset s \land s \subset u) \leftrightarrow \neg \exists s \in S (t \subset s \land s \subset u))$
12	11	anbi2d	$⊢ w = W \to ((t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)) \leftrightarrow (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))$
13	9 12	anbi12d	$⊢ w = W \to (((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u))) \leftrightarrow ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u))))$
14	13	opabbidv	$⊢ w = W \to \{⟨t, u⟩ \| ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)))\} = \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\}$
15		df-lcv	$⊢ ⋖_{L} = (w \in V ⟼ \{⟨t, u⟩ \| ((t \in LSubSp (w) \land u \in LSubSp (w)) \land (t \subset u \land \neg \exists s \in LSubSp (w) (t \subset s \land s \subset u)))\})$
16	1	fvexi	$⊢ S \in V$
17	16 16	xpex	$⊢ S \times S \in V$
18		opabssxp	$⊢ \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\} \subseteq S \times S$
19	17 18	ssexi	$⊢ \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\} \in V$
20	14 15 19	fvmpt	$⊢ W \in V \to ⋖_{L} (W) = \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\}$
21	3 4 20	3syl	$⊢ φ \to ⋖_{L} (W) = \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\}$
22	2 21	syl5eq	$⊢ φ \to C = \{⟨t, u⟩ \| ((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)))\}$

Metamath Proof Explorer

Theorem lcvfbr

Proof