Metamath Proof Explorer


Theorem lshpkrcl

Description: The set G defined by hyperplane U is a linear functional. (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.f F = LFnl W
Assertion lshpkrcl φ G F

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.f F = LFnl W
15 6 adantr φ a V W LVec
16 7 adantr φ a V U H
17 8 adantr φ a V Z V
18 simpr φ a V a V
19 9 adantr φ a V U ˙ N Z = V
20 1 2 3 4 5 15 16 17 18 19 10 11 12 lshpsmreu φ a V ∃! k K y U a = y + ˙ k · ˙ Z
21 riotacl ∃! k K y U a = y + ˙ k · ˙ Z ι k K | y U a = y + ˙ k · ˙ Z K
22 20 21 syl φ a V ι k K | y U a = y + ˙ k · ˙ Z K
23 eqeq1 x = a x = y + ˙ k · ˙ Z a = y + ˙ k · ˙ Z
24 23 rexbidv x = a y U x = y + ˙ k · ˙ Z y U a = y + ˙ k · ˙ Z
25 24 riotabidv x = a ι k K | y U x = y + ˙ k · ˙ Z = ι k K | y U a = y + ˙ k · ˙ Z
26 25 cbvmptv x V ι k K | y U x = y + ˙ k · ˙ Z = a V ι k K | y U a = y + ˙ k · ˙ Z
27 13 26 eqtri G = a V ι k K | y U a = y + ˙ k · ˙ Z
28 22 27 fmptd φ G : V K
29 eqid 0 D = 0 D
30 1 2 3 4 5 6 7 8 8 9 10 11 12 29 13 lshpkrlem6 φ l K u V v V G l · ˙ u + ˙ v = l D G u + D G v
31 30 ralrimivvva φ l K u V v V G l · ˙ u + ˙ v = l D G u + D G v
32 eqid + D = + D
33 eqid D = D
34 1 2 10 12 11 32 33 14 islfl W LVec G F G : V K l K u V v V G l · ˙ u + ˙ v = l D G u + D G v
35 6 34 syl φ G F G : V K l K u V v V G l · ˙ u + ˙ v = l D G u + D G v
36 28 31 35 mpbir2and φ G F