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 ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpkrex.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lshpkrex.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion lshpkrex ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) → ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 lshpkrex.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
2 lshpkrex.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
3 lshpkrex.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
4 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
6 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
7 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
8 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9 4 5 6 7 1 8 islshpsm ⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐻 ↔ ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑈 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) ) )
10 simp3 ⊢ ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑈 ≠ ( Base ‘ 𝑊 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → ∃ 𝑧 ∈ ( Base ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) )
11 9 10 biimtrdi ⊢ ( 𝑊 ∈ LVec → ( 𝑈 ∈ 𝐻 → ∃ 𝑧 ∈ ( Base ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) )
12 11 imp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) → ∃ 𝑧 ∈ ( Base ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) )
13 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
14 simp1l ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → 𝑊 ∈ LVec )
15 simp1r ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → 𝑈 ∈ 𝐻 )
16 simp2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
17 simp3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) )
18 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
19 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
20 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
21 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) )
22 4 13 5 7 1 14 15 16 17 18 19 20 21 2 lshpkrcl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) ∈ 𝐹 )
23 4 13 5 7 1 14 15 16 17 18 19 20 21 3 lshpkr ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → ( 𝐾 ‘ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) ) = 𝑈 )
24 fveqeq2 ⊢ ( 𝑔 = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) → ( ( 𝐾 ‘ 𝑔 ) = 𝑈 ↔ ( 𝐾 ‘ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) ) = 𝑈 ) )
25 24 rspcev ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) ∈ 𝐹 ∧ ( 𝐾 ‘ ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ℩ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 ( +g ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑧 ) ) ) ) ) = 𝑈 ) → ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑈 )
26 22 23 25 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ∧ ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) ) → ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑈 )
27 26 rexlimdv3a ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) → ( ∃ 𝑧 ∈ ( Base ‘ 𝑊 ) ( 𝑈 ( LSSum ‘ 𝑊 ) ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) = ( Base ‘ 𝑊 ) → ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑈 ) )
28 12 27 mpd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑈 ∈ 𝐻 ) → ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑈 )