Metamath Proof Explorer

Theorem 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 ∈ X → H = s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ 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 ∈ X → W ∈ V
6 fveq2 ⊢ w = W → LSubSp ⁡ w = LSubSp ⁡ W
7 6 3 eqtr4di ⊢ w = W → LSubSp ⁡ w = S
8 fveq2 ⊢ w = W → Base w = Base W
9 8 1 eqtr4di ⊢ w = W → Base w = V
10 9 neeq2d ⊢ w = W → s ≠ Base w ↔ s ≠ V
11 fveq2 ⊢ w = W → LSpan ⁡ w = LSpan ⁡ W
12 11 2 eqtr4di ⊢ w = W → LSpan ⁡ w = N
13 12 fveq1d ⊢ w = W → LSpan ⁡ w ⁡ s ∪ v = N ⁡ s ∪ v
14 13 9 eqeq12d ⊢ w = W → LSpan ⁡ w ⁡ s ∪ v = Base w ↔ N ⁡ s ∪ v = V
15 9 14 rexeqbidv ⊢ w = W → ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w ↔ ∃ v ∈ V N ⁡ s ∪ v = V
16 10 15 anbi12d ⊢ w = W → s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w ↔ s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V
17 7 16 rabeqbidv ⊢ w = W → s ∈ LSubSp ⁡ w | s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w = s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V
18 df-lshyp ⊢ LSHyp = w ∈ V ⟼ s ∈ LSubSp ⁡ w | s ≠ Base w ∧ ∃ v ∈ Base w LSpan ⁡ w ⁡ s ∪ v = Base w
19 3 fvexi ⊢ S ∈ V
20 19 rabex ⊢ s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V ∈ V
21 17 18 20 fvmpt ⊢ W ∈ V → LSHyp ⁡ W = s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V
22 5 21 syl ⊢ W ∈ X → LSHyp ⁡ W = s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V
23 4 22 eqtrid ⊢ W ∈ X → H = s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V