Metamath Proof Explorer


Theorem lshpkr

Description: The kernel of functional G is the hyperplane defining it. (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lshpkr.v V = Base W
lshpkr.a + ˙ = + W
lshpkr.n N = LSpan W
lshpkr.p ˙ = LSSum W
lshpkr.h H = LSHyp W
lshpkr.w φ W LVec
lshpkr.u φ U H
lshpkr.z φ Z V
lshpkr.e φ U ˙ N Z = V
lshpkr.d D = Scalar W
lshpkr.k K = Base D
lshpkr.t · ˙ = W
lshpkr.g G = x V ι k K | y U x = y + ˙ k · ˙ Z
lshpkr.l L = LKer W
Assertion lshpkr φ L G = U

Proof

Step Hyp Ref Expression
1 lshpkr.v V = Base W
2 lshpkr.a + ˙ = + W
3 lshpkr.n N = LSpan W
4 lshpkr.p ˙ = LSSum W
5 lshpkr.h H = LSHyp W
6 lshpkr.w φ W LVec
7 lshpkr.u φ U H
8 lshpkr.z φ Z V
9 lshpkr.e φ U ˙ N Z = V
10 lshpkr.d D = Scalar W
11 lshpkr.k K = Base D
12 lshpkr.t · ˙ = W
13 lshpkr.g G = x V ι k K | y U x = y + ˙ k · ˙ Z
14 lshpkr.l L = LKer W
15 eqid LFnl W = LFnl W
16 lveclmod W LVec W LMod
17 6 16 syl φ W LMod
18 1 2 3 4 5 6 7 8 9 10 11 12 13 15 lshpkrcl φ G LFnl W
19 1 15 14 17 18 lkrssv φ L G V
20 19 sseld φ v L G v V
21 eqid LSubSp W = LSubSp W
22 21 5 17 7 lshplss φ U LSubSp W
23 1 21 lssel U LSubSp W v U v V
24 22 23 sylan φ v U v V
25 24 ex φ v U v V
26 eqid 0 D = 0 D
27 1 10 26 15 14 ellkr W LVec G LFnl W v L G v V G v = 0 D
28 6 18 27 syl2anc φ v L G v V G v = 0 D
29 28 baibd φ v V v L G G v = 0 D
30 6 adantr φ v V W LVec
31 7 adantr φ v V U H
32 8 adantr φ v V Z V
33 simpr φ v V v V
34 9 adantr φ v V U ˙ N Z = V
35 1 2 3 4 5 30 31 32 33 34 10 11 12 26 13 lshpkrlem1 φ v V v U G v = 0 D
36 29 35 bitr4d φ v V v L G v U
37 36 ex φ v V v L G v U
38 20 25 37 pm5.21ndd φ v L G v U
39 38 eqrdv φ L G = U