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	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐾 )