lcvbr3

Description: The covers relation for a left vector space (or a left module). (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	lcvbr3	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \forall s \in S ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = 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	1 2 3 4 5	lcvbr	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \neg \exists s \in S (T \subset s \land s \subset U)))$
7		iman	$⊢ ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = U)) \leftrightarrow \neg ((T \subseteq s \land s \subseteq U) \land \neg (s = T \lor s = U))$
8		df-pss	$⊢ T \subset s \leftrightarrow (T \subseteq s \land T \neq s)$
9		necom	$⊢ T \neq s \leftrightarrow s \neq T$
10	9	anbi2i	$⊢ (T \subseteq s \land T \neq s) \leftrightarrow (T \subseteq s \land s \neq T)$
11	8 10	bitri	$⊢ T \subset s \leftrightarrow (T \subseteq s \land s \neq T)$
12		df-pss	$⊢ s \subset U \leftrightarrow (s \subseteq U \land s \neq U)$
13	11 12	anbi12i	$⊢ (T \subset s \land s \subset U) \leftrightarrow ((T \subseteq s \land s \neq T) \land (s \subseteq U \land s \neq U))$
14		an4	$⊢ ((T \subseteq s \land s \neq T) \land (s \subseteq U \land s \neq U)) \leftrightarrow ((T \subseteq s \land s \subseteq U) \land (s \neq T \land s \neq U))$
15		neanior	$⊢ (s \neq T \land s \neq U) \leftrightarrow \neg (s = T \lor s = U)$
16	15	anbi2i	$⊢ ((T \subseteq s \land s \subseteq U) \land (s \neq T \land s \neq U)) \leftrightarrow ((T \subseteq s \land s \subseteq U) \land \neg (s = T \lor s = U))$
17	14 16	bitri	$⊢ ((T \subseteq s \land s \neq T) \land (s \subseteq U \land s \neq U)) \leftrightarrow ((T \subseteq s \land s \subseteq U) \land \neg (s = T \lor s = U))$
18	13 17	bitri	$⊢ (T \subset s \land s \subset U) \leftrightarrow ((T \subseteq s \land s \subseteq U) \land \neg (s = T \lor s = U))$
19	7 18	xchbinxr	$⊢ ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = U)) \leftrightarrow \neg (T \subset s \land s \subset U)$
20	19	ralbii	$⊢ \forall s \in S ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = U)) \leftrightarrow \forall s \in S \neg (T \subset s \land s \subset U)$
21		ralnex	$⊢ \forall s \in S \neg (T \subset s \land s \subset U) \leftrightarrow \neg \exists s \in S (T \subset s \land s \subset U)$
22	20 21	bitri	$⊢ \forall s \in S ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = U)) \leftrightarrow \neg \exists s \in S (T \subset s \land s \subset U)$
23	22	anbi2i	$⊢ (T \subset U \land \forall s \in S ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = U))) \leftrightarrow (T \subset U \land \neg \exists s \in S (T \subset s \land s \subset U))$
24	6 23	bitr4di	$⊢ φ \to (T C U \leftrightarrow (T \subset U \land \forall s \in S ((T \subseteq s \land s \subseteq U) \to (s = T \lor s = U))))$

Metamath Proof Explorer

Theorem lcvbr3

Proof