Theorem hdmapellkr

Description: Membership in the kernel (as shown by hdmaplkr ) of the vector to dual map. Line 17 in Holland95 p. 14. (Contributed by NM, 16-Jun-2015)

	Ref	Expression
Hypotheses	hdmapellkr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapellkr.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapellkr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapellkr.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapellkr.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapellkr.z	⊢ 0 = ( 0g ‘ 𝑅 )
	hdmapellkr.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapellkr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapellkr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmapellkr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	hdmapellkr	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 0 ↔ 𝑌 ∈ ( 𝑂 ‘ { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapellkr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapellkr.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmapellkr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmapellkr.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		hdmapellkr.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6		hdmapellkr.z	⊢ 0 = ( 0g ‘ 𝑅 )
7		hdmapellkr.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8		hdmapellkr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		hdmapellkr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		hdmapellkr.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
12		eqid	⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
13	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14		eqid	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
15		eqid	⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
16	1 3 4 14 15 7 8 9	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
17	1 14 15 3 11 8 16	lcdvbaselfl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) )
18	4 5 6 11 12 13 17 10	ellkr2	⊢ ( 𝜑 → ( 𝑌 ∈ ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) ↔ ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 0 ) )
19	1 2 3 4 11 12 7 8 9	hdmaplkr	⊢ ( 𝜑 → ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) = ( 𝑂 ‘ { 𝑋 } ) )
20	19	eleq2d	⊢ ( 𝜑 → ( 𝑌 ∈ ( ( LKer ‘ 𝑈 ) ‘ ( 𝑆 ‘ 𝑋 ) ) ↔ 𝑌 ∈ ( 𝑂 ‘ { 𝑋 } ) ) )
21	18 20	bitr3d	⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝑋 ) ‘ 𝑌 ) = 0 ↔ 𝑌 ∈ ( 𝑂 ‘ { 𝑋 } ) ) )