Metamath Proof Explorer

Theorem 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 ∈ X → U ∈ H ↔ U ∈ S ∧ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ 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 1 2 3 4 lshpset ⊢ W ∈ X → H = s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V
6 5 eleq2d ⊢ W ∈ X → U ∈ H ↔ U ∈ s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V
7 neeq1 ⊢ s = U → s ≠ V ↔ U ≠ V
8 uneq1 ⊢ s = U → s ∪ v = U ∪ v
9 8 fveqeq2d ⊢ s = U → N ⁡ s ∪ v = V ↔ N ⁡ U ∪ v = V
10 9 rexbidv ⊢ s = U → ∃ v ∈ V N ⁡ s ∪ v = V ↔ ∃ v ∈ V N ⁡ U ∪ v = V
11 7 10 anbi12d ⊢ s = U → s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V ↔ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ v = V
12 11 elrab ⊢ U ∈ s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V ↔ U ∈ S ∧ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ v = V
13 3anass ⊢ U ∈ S ∧ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ v = V ↔ U ∈ S ∧ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ v = V
14 12 13 bitr4i ⊢ U ∈ s ∈ S | s ≠ V ∧ ∃ v ∈ V N ⁡ s ∪ v = V ↔ U ∈ S ∧ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ v = V
15 6 14 bitrdi ⊢ W ∈ X → U ∈ H ↔ U ∈ S ∧ U ≠ V ∧ ∃ v ∈ V N ⁡ U ∪ v = V