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

Metamath Proof Explorer

Theorem lshpkrlem2

Description: Lemma for lshpkrex . The value of tentative functional G is a scalar. (Contributed by NM, 16-Jul-2014)

Ref Expression
Hypotheses lshpkrlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpkrlem.a ⊢ + = ( +g ‘ 𝑊 )
lshpkrlem.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpkrlem.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpkrlem.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpkrlem.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpkrlem.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
lshpkrlem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lshpkrlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lshpkrlem.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
lshpkrlem.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lshpkrlem.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lshpkrlem.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lshpkrlem.o ⊢ 0 = ( 0g ‘ 𝐷 )
lshpkrlem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
Assertion lshpkrlem2 ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 lshpkrlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpkrlem.a ⊢ + = ( +g ‘ 𝑊 )
3 lshpkrlem.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lshpkrlem.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lshpkrlem.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6 lshpkrlem.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lshpkrlem.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
8 lshpkrlem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 lshpkrlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lshpkrlem.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
11 lshpkrlem.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
12 lshpkrlem.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
13 lshpkrlem.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
14 lshpkrlem.o ⊢ 0 = ( 0g ‘ 𝐷 )
15 lshpkrlem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
16 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
17 16 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
18 17 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
19 riotaex ⊢ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ∈ V
20 18 15 19 fvmpt ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
21 9 20 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
22 1 2 3 4 5 6 7 8 9 10 11 12 13 lshpsmreu ⊢ ( 𝜑 → ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )
23 riotacl ⊢ ( ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ∈ 𝐾 )
24 22 23 syl ⊢ ( 𝜑 → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ∈ 𝐾 )
25 21 24 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 )