This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpkr.a ⊢ + = ( +g ‘ 𝑊 )
lshpkr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpkr.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpkr.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpkr.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpkr.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
lshpkr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lshpkr.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
lshpkr.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lshpkr.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lshpkr.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lshpkr.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
lshpkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
Assertion lshpkrcl ( 𝜑 → 𝐺 ∈ 𝐹 )

Proof

Step Hyp Ref Expression
1 lshpkr.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpkr.a ⊢ + = ( +g ‘ 𝑊 )
3 lshpkr.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lshpkr.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lshpkr.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6 lshpkr.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lshpkr.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
8 lshpkr.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 lshpkr.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
10 lshpkr.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
11 lshpkr.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
12 lshpkr.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
13 lshpkr.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
14 lshpkr.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
15 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → 𝑊 ∈ LVec )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → 𝑈 ∈ 𝐻 )
17 8 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → 𝑍 ∈ 𝑉 )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
19 9 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
20 1 2 3 4 5 15 16 17 18 19 10 11 12 lshpsmreu ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )
21 riotacl ⊢ ( ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ∈ 𝐾 )
22 20 21 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑉 ) → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ∈ 𝐾 )
23 eqeq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
24 23 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
25 24 riotabidv ⊢ ( 𝑥 = 𝑎 → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
26 25 cbvmptv ⊢ ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ) = ( 𝑎 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
27 13 26 eqtri ⊢ 𝐺 = ( 𝑎 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑎 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
28 22 27 fmptd ⊢ ( 𝜑 → 𝐺 : 𝑉 ⟶ 𝐾 )
29 eqid ⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
30 1 2 3 4 5 6 7 8 8 9 10 11 12 29 13 lshpkrlem6 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ 𝐾 ∧ 𝑢 ∈ 𝑉 ∧ 𝑣 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )
31 30 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑙 ∈ 𝐾 ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) )
32 eqid ⊢ ( +g ‘ 𝐷 ) = ( +g ‘ 𝐷 )
33 eqid ⊢ ( .r ‘ 𝐷 ) = ( .r ‘ 𝐷 )
34 1 2 10 12 11 32 33 14 islfl ⊢ ( 𝑊 ∈ LVec → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑙 ∈ 𝐾 ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) ) )
35 6 34 syl ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐹 ↔ ( 𝐺 : 𝑉 ⟶ 𝐾 ∧ ∀ 𝑙 ∈ 𝐾 ∀ 𝑢 ∈ 𝑉 ∀ 𝑣 ∈ 𝑉 ( 𝐺 ‘ ( ( 𝑙 · 𝑢 ) + 𝑣 ) ) = ( ( 𝑙 ( .r ‘ 𝐷 ) ( 𝐺 ‘ 𝑢 ) ) ( +g ‘ 𝐷 ) ( 𝐺 ‘ 𝑣 ) ) ) ) )
36 28 31 35 mpbir2and ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )