Metamath Proof Explorer


Theorem lshpset2N

Description: The set of all hyperplanes of a left module or left vector space equals the set of all kernels of nonzero functionals. (Contributed by NM, 17-Jul-2014) (New usage is discouraged.)

Ref Expression
Hypotheses lshpset2.v V = Base W
lshpset2.d D = Scalar W
lshpset2.z 0 ˙ = 0 D
lshpset2.h H = LSHyp W
lshpset2.f F = LFnl W
lshpset2.k K = LKer W
Assertion lshpset2N W LVec H = s | g F g V × 0 ˙ s = K g

Proof

Step Hyp Ref Expression
1 lshpset2.v V = Base W
2 lshpset2.d D = Scalar W
3 lshpset2.z 0 ˙ = 0 D
4 lshpset2.h H = LSHyp W
5 lshpset2.f F = LFnl W
6 lshpset2.k K = LKer W
7 4 5 6 lshpkrex W LVec s H g F K g = s
8 eleq1 K g = s K g H s H
9 8 biimparc s H K g = s K g H
10 9 adantll W LVec s H K g = s K g H
11 10 adantlr W LVec s H g F K g = s K g H
12 simplll W LVec s H g F K g = s W LVec
13 simplr W LVec s H g F K g = s g F
14 1 2 3 4 5 6 12 13 lkrshp3 W LVec s H g F K g = s K g H g V × 0 ˙
15 11 14 mpbid W LVec s H g F K g = s g V × 0 ˙
16 15 ex W LVec s H g F K g = s g V × 0 ˙
17 eqimss2 K g = s s K g
18 eqimss K g = s K g s
19 17 18 eqssd K g = s s = K g
20 19 a1i W LVec s H g F K g = s s = K g
21 16 20 jcad W LVec s H g F K g = s g V × 0 ˙ s = K g
22 21 reximdva W LVec s H g F K g = s g F g V × 0 ˙ s = K g
23 7 22 mpd W LVec s H g F g V × 0 ˙ s = K g
24 23 ex W LVec s H g F g V × 0 ˙ s = K g
25 1 2 3 4 5 6 lkrshp W LVec g F g V × 0 ˙ K g H
26 25 3adant3r W LVec g F g V × 0 ˙ s = K g K g H
27 eqid LSpan W = LSpan W
28 eqid LSubSp W = LSubSp W
29 1 27 28 4 islshp W LVec K g H K g LSubSp W K g V v V LSpan W K g v = V
30 29 3ad2ant1 W LVec g F g V × 0 ˙ s = K g K g H K g LSubSp W K g V v V LSpan W K g v = V
31 26 30 mpbid W LVec g F g V × 0 ˙ s = K g K g LSubSp W K g V v V LSpan W K g v = V
32 eleq1 s = K g s LSubSp W K g LSubSp W
33 neeq1 s = K g s V K g V
34 uneq1 s = K g s v = K g v
35 34 fveqeq2d s = K g LSpan W s v = V LSpan W K g v = V
36 35 rexbidv s = K g v V LSpan W s v = V v V LSpan W K g v = V
37 32 33 36 3anbi123d s = K g s LSubSp W s V v V LSpan W s v = V K g LSubSp W K g V v V LSpan W K g v = V
38 37 adantl g V × 0 ˙ s = K g s LSubSp W s V v V LSpan W s v = V K g LSubSp W K g V v V LSpan W K g v = V
39 38 3ad2ant3 W LVec g F g V × 0 ˙ s = K g s LSubSp W s V v V LSpan W s v = V K g LSubSp W K g V v V LSpan W K g v = V
40 31 39 mpbird W LVec g F g V × 0 ˙ s = K g s LSubSp W s V v V LSpan W s v = V
41 40 rexlimdv3a W LVec g F g V × 0 ˙ s = K g s LSubSp W s V v V LSpan W s v = V
42 1 27 28 4 islshp W LVec s H s LSubSp W s V v V LSpan W s v = V
43 41 42 sylibrd W LVec g F g V × 0 ˙ s = K g s H
44 24 43 impbid W LVec s H g F g V × 0 ˙ s = K g
45 44 abbi2dv W LVec H = s | g F g V × 0 ˙ s = K g