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	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )