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