Theorem lshpkr

Description: The kernel of functional G is the hyperplane defining it. (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.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
Assertion	lshpkr	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = 𝑈 )

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.l	⊢ 𝐿 = ( LKer ‘ 𝑊 )
15		eqid	⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
16		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
17	6 16	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
18	1 2 3 4 5 6 7 8 9 10 11 12 13 15	lshpkrcl	⊢ ( 𝜑 → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
19	1 15 14 17 18	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
20	19	sseld	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) → 𝑣 ∈ 𝑉 ) )
21		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
22	21 5 17 7	lshplss	⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
23	1 21	lssel	⊢ ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ∈ 𝑉 )
24	22 23	sylan	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ∈ 𝑉 )
25	24	ex	⊢ ( 𝜑 → ( 𝑣 ∈ 𝑈 → 𝑣 ∈ 𝑉 ) )
26		eqid	⊢ ( 0g ‘ 𝐷 ) = ( 0g ‘ 𝐷 )
27	1 10 26 15 14	ellkr	⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ ( LFnl ‘ 𝑊 ) ) → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 0g ‘ 𝐷 ) ) ) )
28	6 18 27	syl2anc	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 0g ‘ 𝐷 ) ) ) )
29	28	baibd	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ ( 𝐺 ‘ 𝑣 ) = ( 0g ‘ 𝐷 ) ) )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑊 ∈ LVec )
31	7	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ∈ 𝐻 )
32	8	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑍 ∈ 𝑉 )
33		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
34	9	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
35	1 2 3 4 5 30 31 32 33 34 10 11 12 26 13	lshpkrlem1	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ∈ 𝑈 ↔ ( 𝐺 ‘ 𝑣 ) = ( 0g ‘ 𝐷 ) ) )
36	29 35	bitr4d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ 𝑣 ∈ 𝑈 ) )
37	36	ex	⊢ ( 𝜑 → ( 𝑣 ∈ 𝑉 → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ 𝑣 ∈ 𝑈 ) ) )
38	20 25 37	pm5.21ndd	⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝐿 ‘ 𝐺 ) ↔ 𝑣 ∈ 𝑈 ) )
39	38	eqrdv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = 𝑈 )