islshp

Description: The predicate "is a hyperplane" (of a left module or left vector space). (Contributed by NM, 29-Jun-2014)

	Ref	Expression
Hypotheses	lshpset.v	$⊢ V = {Base}_{W}$
	lshpset.n	$⊢ N = LSpan (W)$
	lshpset.s	$⊢ S = LSubSp (W)$
	lshpset.h	$⊢ H = LSHyp (W)$
Assertion	islshp	$⊢ W \in X \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$

Step	Hyp	Ref	Expression
1		lshpset.v	$⊢ V = {Base}_{W}$
2		lshpset.n	$⊢ N = LSpan (W)$
3		lshpset.s	$⊢ S = LSubSp (W)$
4		lshpset.h	$⊢ H = LSHyp (W)$
5	1 2 3 4	lshpset	$⊢ W \in X \to H = \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\}$
6	5	eleq2d	$⊢ W \in X \to (U \in H \leftrightarrow U \in \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\})$
7		neeq1	$⊢ s = U \to (s \neq V \leftrightarrow U \neq V)$
8		uneq1	$⊢ s = U \to s \cup \{v\} = U \cup \{v\}$
9	8	fveqeq2d	$⊢ s = U \to (N (s \cup \{v\}) = V \leftrightarrow N (U \cup \{v\}) = V)$
10	9	rexbidv	$⊢ s = U \to (\exists v \in V N (s \cup \{v\}) = V \leftrightarrow \exists v \in V N (U \cup \{v\}) = V)$
11	7 10	anbi12d	$⊢ s = U \to ((s \neq V \land \exists v \in V N (s \cup \{v\}) = V) \leftrightarrow (U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
12	11	elrab	$⊢ U \in \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\} \leftrightarrow (U \in S \land (U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
13		3anass	$⊢ (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V) \leftrightarrow (U \in S \land (U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$
14	12 13	bitr4i	$⊢ U \in \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\} \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V)$
15	6 14	bitrdi	$⊢ W \in X \to (U \in H \leftrightarrow (U \in S \land U \neq V \land \exists v \in V N (U \cup \{v\}) = V))$

Metamath Proof Explorer