Theorem dochsnkr2

Description: Kernel of the explicit functional G determined by a nonzero vector X . Compare the more general lshpkr . (Contributed by NM, 27-Oct-2014)

	Ref	Expression
Hypotheses	dochsnkr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochsnkr2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochsnkr2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochsnkr2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochsnkr2.z	⊢ 0 = ( 0g ‘ 𝑈 )
	dochsnkr2.a	⊢ + = ( +g ‘ 𝑈 )
	dochsnkr2.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	dochsnkr2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	dochsnkr2.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
	dochsnkr2.r	⊢ 𝑅 = ( Base ‘ 𝐷 )
	dochsnkr2.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
	dochsnkr2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochsnkr2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion	dochsnkr2	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		dochsnkr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochsnkr2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochsnkr2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochsnkr2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochsnkr2.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		dochsnkr2.a	⊢ + = ( +g ‘ 𝑈 )
7		dochsnkr2.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
8		dochsnkr2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
9		dochsnkr2.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
10		dochsnkr2.r	⊢ 𝑅 = ( Base ‘ 𝐷 )
11		dochsnkr2.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
12		dochsnkr2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		dochsnkr2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
15		eqid	⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
16		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
17	1 3 12	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
18	1 2 3 4 5 16 12 13	dochsnshp	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
19	13	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
20	1 2 3 4 5 14 15 12 13	dochexmidat	⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = 𝑉 )
21	4 6 14 15 16 17 18 19 20 9 10 7 11 8	lshpkr	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )