lshpset

Description: The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (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	lshpset	$⊢ W \in X \to H = \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\}$

Proof

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		elex	$⊢ W \in X \to W \in V$
6		fveq2	$⊢ w = W \to LSubSp (w) = LSubSp (W)$
7	6 3	eqtr4di	$⊢ w = W \to LSubSp (w) = S$
8		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
9	8 1	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
10	9	neeq2d	$⊢ w = W \to (s \neq {Base}_{w} \leftrightarrow s \neq V)$
11		fveq2	$⊢ w = W \to LSpan (w) = LSpan (W)$
12	11 2	eqtr4di	$⊢ w = W \to LSpan (w) = N$
13	12	fveq1d	$⊢ w = W \to LSpan (w) (s \cup \{v\}) = N (s \cup \{v\})$
14	13 9	eqeq12d	$⊢ w = W \to (LSpan (w) (s \cup \{v\}) = {Base}_{w} \leftrightarrow N (s \cup \{v\}) = V)$
15	9 14	rexeqbidv	$⊢ w = W \to (\exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w} \leftrightarrow \exists v \in V N (s \cup \{v\}) = V)$
16	10 15	anbi12d	$⊢ w = W \to ((s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w}) \leftrightarrow (s \neq V \land \exists v \in V N (s \cup \{v\}) = V))$
17	7 16	rabeqbidv	$⊢ w = W \to \{s \in LSubSp (w) \| (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})\} = \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\}$
18		df-lshyp	$⊢ LSHyp = (w \in V ⟼ \{s \in LSubSp (w) \| (s \neq {Base}_{w} \land \exists v \in {Base}_{w} LSpan (w) (s \cup \{v\}) = {Base}_{w})\})$
19	3	fvexi	$⊢ S \in V$
20	19	rabex	$⊢ \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\} \in V$
21	17 18 20	fvmpt	$⊢ W \in V \to LSHyp (W) = \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\}$
22	5 21	syl	$⊢ W \in X \to LSHyp (W) = \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\}$
23	4 22	eqtrid	$⊢ W \in X \to H = \{s \in S \| (s \neq V \land \exists v \in V N (s \cup \{v\}) = V)\}$

Metamath Proof Explorer

Theorem lshpset

Proof