Theorem hdmaplkr

Description: Kernel of the vector to dual map. Line 16 in Holland95 p. 14. TODO: eliminate F hypothesis. (Contributed by NM, 9-Jun-2015)

	Ref	Expression
Hypotheses	hdmaplkr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmaplkr.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	hdmaplkr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmaplkr.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmaplkr.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	hdmaplkr.y	⊢ 𝑌 = ( LKer ‘ 𝑈 )
	hdmaplkr.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmaplkr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmaplkr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion	hdmaplkr	⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) = ( 𝑂 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		hdmaplkr.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmaplkr.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmaplkr.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		hdmaplkr.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		hdmaplkr.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		hdmaplkr.y	⊢ 𝑌 = ( LKer ‘ 𝑈 )
7		hdmaplkr.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8		hdmaplkr.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		hdmaplkr.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		fveq2	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑆 ‘ 𝑋 ) = ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) )
11	10	fveq2d	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) = ( 𝑌 ‘ ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ) )
12		sneq	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑋 } = { ( 0g ‘ 𝑈 ) } )
13	12	fveq2d	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( 𝑂 ‘ { 𝑋 } ) = ( 𝑂 ‘ { ( 0g ‘ 𝑈 ) } ) )
14	11 13	sseq12d	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ { 𝑋 } ) ↔ ( 𝑌 ‘ ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ) ⊆ ( 𝑂 ‘ { ( 0g ‘ 𝑈 ) } ) ) )
15		eqid	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
16	1 15 8	lcdlmod	⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
17		eqid	⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
18	1 3 4 15 17 7 8 9	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
19		eqid	⊢ ( LSpan ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSpan ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
20	17 19	lspsnid	⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑆 ‘ 𝑋 ) ∈ ( ( LSpan ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { ( 𝑆 ‘ 𝑋 ) } ) )
21	16 18 20	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( ( LSpan ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { ( 𝑆 ‘ 𝑋 ) } ) )
22		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
23		eqid	⊢ ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
24	1 3 4 22 15 19 23 7 8 9	hdmap10	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ( LSpan ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { ( 𝑆 ‘ 𝑋 ) } ) )
25		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
26	1 2 23 3 4 22 25 6 8 9	mapdsn	⊢ ( 𝜑 → ( ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ 𝑓 ) } )
27	24 26	eqtr3d	⊢ ( 𝜑 → ( ( LSpan ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { ( 𝑆 ‘ 𝑋 ) } ) = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ 𝑓 ) } )
28	21 27	eleqtrd	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ 𝑓 ) } )
29	1 15 17 3 25 8 18	lcdvbaselfl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) )
30		fveq2	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑋 ) → ( 𝑌 ‘ 𝑓 ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) )
31	30	sseq2d	⊢ ( 𝑓 = ( 𝑆 ‘ 𝑋 ) → ( ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ 𝑓 ) ↔ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ) )
32	31	elrab3	⊢ ( ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) → ( ( 𝑆 ‘ 𝑋 ) ∈ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ 𝑓 ) } ↔ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ) )
33	29 32	syl	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ∈ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ 𝑓 ) } ↔ ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ) )
34	28 33	mpbid	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) )
36		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
37	1 3 8	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑈 ∈ LVec )
39		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
40	8	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
41	9	anim1i	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) )
42		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) )
43	41 42	sylibr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
44	1 2 3 4 39 36 40 43	dochsnshp	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑂 ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
45	29	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) )
46		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
47		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) )
48		eqid	⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
49	1 3 4 46 47 15 48 8	lcd0v	⊢ ( 𝜑 → ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) )
50	49	eqeq2d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( 𝑆 ‘ 𝑋 ) = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) )
51	1 3 4 39 15 48 7 8 9	hdmapeq0	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝑋 = ( 0g ‘ 𝑈 ) ) )
52	50 51	bitr3d	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ↔ 𝑋 = ( 0g ‘ 𝑈 ) ) )
53	52	necon3bid	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑋 ) ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ↔ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) )
54	53	biimpar	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑆 ‘ 𝑋 ) ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) )
55	4 46 47 36 25 6	lkrshp	⊢ ( ( 𝑈 ∈ LVec ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) ∧ ( 𝑆 ‘ 𝑋 ) ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑈 ) ) } ) ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ∈ ( LSHyp ‘ 𝑈 ) )
56	38 45 54 55	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ∈ ( LSHyp ‘ 𝑈 ) )
57	36 38 44 56	lshpcmp	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝑂 ‘ { 𝑋 } ) ⊆ ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ { 𝑋 } ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ) )
58	35 57	mpbid	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑂 ‘ { 𝑋 } ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) )
59		eqimss2	⊢ ( ( 𝑂 ‘ { 𝑋 } ) = ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ { 𝑋 } ) )
60	58 59	syl	⊢ ( ( 𝜑 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ { 𝑋 } ) )
61	1 3 8	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
62	4 39	lmod0vcl	⊢ ( 𝑈 ∈ LMod → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
63	61 62	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) ∈ 𝑉 )
64	1 3 4 15 17 7 8 63	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
65	1 15 17 3 25 8 64	lcdvbaselfl	⊢ ( 𝜑 → ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ∈ ( LFnl ‘ 𝑈 ) )
66	4 25 6 61 65	lkrssv	⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ) ⊆ 𝑉 )
67	1 3 2 4 39	doch0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑂 ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
68	8 67	syl	⊢ ( 𝜑 → ( 𝑂 ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
69	66 68	sseqtrrd	⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝑆 ‘ ( 0g ‘ 𝑈 ) ) ) ⊆ ( 𝑂 ‘ { ( 0g ‘ 𝑈 ) } ) )
70	14 60 69	pm2.61ne	⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) ⊆ ( 𝑂 ‘ { 𝑋 } ) )
71	70 34	eqssd	⊢ ( 𝜑 → ( 𝑌 ‘ ( 𝑆 ‘ 𝑋 ) ) = ( 𝑂 ‘ { 𝑋 } ) )