lcvbr

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

	Ref	Expression
Hypotheses	lcvfbr.s	$⊢ S = LSubSp (W)$
	lcvfbr.c	$⊢ C = ⋖_{L} (W)$
	lcvfbr.w	$⊢ φ \to W \in X$
	lcvfbr.t	$⊢ φ \to T \in S$
	lcvfbr.u	$⊢ φ \to U \in S$
Assertion	lcvbr	$⊢ φ \to (T C U \leftrightarrow (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		lcvfbr.t	$⊢ φ \to T \in S$
5		lcvfbr.u	$⊢ φ \to U \in S$
6		eleq1	$⊢ t = T \to (t \in S \leftrightarrow T \in S)$
7	6	anbi1d	$⊢ t = T \to ((t \in S \land u \in S) \leftrightarrow (T \in S \land u \in S))$
8		psseq1	$⊢ t = T \to (t \subset u \leftrightarrow T \subset u)$
9		psseq1	$⊢ t = T \to (t \subset s \leftrightarrow T \subset s)$
10	9	anbi1d	$⊢ t = T \to ((t \subset s \land s \subset u) \leftrightarrow (T \subset s \land s \subset u))$
11	10	rexbidv	$⊢ t = T \to (\exists s \in S (t \subset s \land s \subset u) \leftrightarrow \exists s \in S (T \subset s \land s \subset u))$
12	11	notbid	$⊢ t = T \to (\neg \exists s \in S (t \subset s \land s \subset u) \leftrightarrow \neg \exists s \in S (T \subset s \land s \subset u))$
13	8 12	anbi12d	$⊢ t = T \to ((t \subset u \land \neg \exists s \in S (t \subset s \land s \subset u)) \leftrightarrow (T \subset u \land \neg \exists s \in S (T \subset s \land s \subset u)))$
14	7 13	anbi12d	$⊢ t = T \to (((t \in S \land u \in S) \land (t \subset u \land \neg \exists s \in S (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))))$
15		eleq1	$⊢ u = U \to (u \in S \leftrightarrow U \in S)$
16	15	anbi2d	$⊢ u = U \to ((T \in S \land u \in S) \leftrightarrow (T \in S \land U \in S))$
17		psseq2	$⊢ u = U \to (T \subset u \leftrightarrow T \subset U)$
18		psseq2	$⊢ u = U \to (s \subset u \leftrightarrow s \subset U)$
19	18	anbi2d	$⊢ u = U \to ((T \subset s \land s \subset u) \leftrightarrow (T \subset s \land s \subset U))$
20	19	rexbidv	$⊢ u = U \to (\exists s \in S (T \subset s \land s \subset u) \leftrightarrow \exists s \in S (T \subset s \land s \subset U))$
21	20	notbid	$⊢ u = U \to (\neg \exists s \in S (T \subset s \land s \subset u) \leftrightarrow \neg \exists s \in S (T \subset s \land s \subset U))$
22	17 21	anbi12d	$⊢ u = U \to ((T \subset u \land \neg \exists s \in S (T \subset s \land s \subset u)) \leftrightarrow (T \subset U \land \neg \exists s \in S (T \subset s \land s \subset U)))$
23	16 22	anbi12d	$⊢ u = U \to (((T \in S \land u \in S) \land (T \subset u \land \neg \exists s \in S (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))))$
24		eqid	$⊢ \{⟨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)))\} = \{⟨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)))\}$
25	14 23 24	brabg	$⊢ (T \in S \land U \in S) \to (T \{⟨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)))\} 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))))$
26	4 5 25	syl2anc	$⊢ φ \to (T \{⟨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)))\} 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))))$
27	1 2 3	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)))\}$
28	27	breqd	$⊢ φ \to (T C U \leftrightarrow T \{⟨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)))\} U)$
29	4 5	jca	$⊢ φ \to (T \in S \land U \in S)$
30	29	biantrurd	$⊢ φ \to ((T \subset U \land \neg \exists s \in S (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))))$
31	26 28 30	3bitr4d	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \neg \exists s \in S (T \subset s \land s \subset U)))$

Metamath Proof Explorer

Theorem lcvbr

Proof