Metamath Proof Explorer

Theorem lshpkrex

Description: There exists a functional whose kernel equals a given hyperplane. Part of Th. 1.27 of Barbu and Precupanu,Convexity and Optimization in Banach Spaces. (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lshpkrex.h ⊢ H = LSHyp ⁡ W
lshpkrex.f ⊢ F = LFnl ⁡ W
lshpkrex.k ⊢ K = LKer ⁡ W
Assertion lshpkrex ⊢ W ∈ LVec ∧ U ∈ H → ∃ g ∈ F K ⁡ g = U

Proof

Step Hyp Ref Expression
1 lshpkrex.h ⊢ H = LSHyp ⁡ W
2 lshpkrex.f ⊢ F = LFnl ⁡ W
3 lshpkrex.k ⊢ K = LKer ⁡ W
4 eqid ⊢ Base W = Base W
5 eqid ⊢ LSpan ⁡ W = LSpan ⁡ W
6 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
7 eqid ⊢ LSSum ⁡ W = LSSum ⁡ W
8 lveclmod ⊢ W ∈ LVec → W ∈ LMod
9 4 5 6 7 1 8 islshpsm ⊢ W ∈ LVec → U ∈ H ↔ U ∈ LSubSp ⁡ W ∧ U ≠ Base W ∧ ∃ z ∈ Base W U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W
10 simp3 ⊢ U ∈ LSubSp ⁡ W ∧ U ≠ Base W ∧ ∃ z ∈ Base W U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → ∃ z ∈ Base W U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W
11 9 10 syl6bi ⊢ W ∈ LVec → U ∈ H → ∃ z ∈ Base W U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W
12 11 imp ⊢ W ∈ LVec ∧ U ∈ H → ∃ z ∈ Base W U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W
13 eqid ⊢ + W = + W
14 simp1l ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → W ∈ LVec
15 simp1r ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → U ∈ H
16 simp2 ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → z ∈ Base W
17 simp3 ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W
18 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
19 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
20 eqid ⊢ ⋅ W = ⋅ W
21 eqid ⊢ x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z = x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z
22 4 13 5 7 1 14 15 16 17 18 19 20 21 2 lshpkrcl ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z ∈ F
23 4 13 5 7 1 14 15 16 17 18 19 20 21 3 lshpkr ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → K ⁡ x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z = U
24 fveqeq2 ⊢ g = x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z → K ⁡ g = U ↔ K ⁡ x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z = U
25 24 rspcev ⊢ x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z ∈ F ∧ K ⁡ x ∈ Base W ⟼ ι k ∈ Base Scalar ⁡ W | ∃ y ∈ U x = y + W k ⋅ W z = U → ∃ g ∈ F K ⁡ g = U
26 22 23 25 syl2anc ⊢ W ∈ LVec ∧ U ∈ H ∧ z ∈ Base W ∧ U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → ∃ g ∈ F K ⁡ g = U
27 26 rexlimdv3a ⊢ W ∈ LVec ∧ U ∈ H → ∃ z ∈ Base W U LSSum ⁡ W LSpan ⁡ W ⁡ z = Base W → ∃ g ∈ F K ⁡ g = U
28 12 27 mpd ⊢ W ∈ LVec ∧ U ∈ H → ∃ g ∈ F K ⁡ g = U