Theorem lcfl9a

Description: Property implying that a functional has a closed kernel. (Contributed by NM, 16-Feb-2015)

	Ref	Expression
Hypotheses	lcfl9a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfl9a.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl9a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl9a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfl9a.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfl9a.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfl9a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfl9a.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	lcfl9a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lcfl9a.s	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝐺 ) )
Assertion	lcfl9a	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl9a.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfl9a.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfl9a.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfl9a.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfl9a.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lcfl9a.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lcfl9a.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		lcfl9a.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9		lcfl9a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10		lcfl9a.s	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝐺 ) )
11	1 3 2 4 7	dochoc1	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
13	1 3 7	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
14	4 5 6 13 8	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
16		sneq	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → { 𝑋 } = { ( 0g ‘ 𝑈 ) } )
17	16	fveq2d	⊢ ( 𝑋 = ( 0g ‘ 𝑈 ) → ( ⊥ ‘ { 𝑋 } ) = ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) )
18		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
19	1 3 2 4 18	doch0	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
20	7 19	syl	⊢ ( 𝜑 → ( ⊥ ‘ { ( 0g ‘ 𝑈 ) } ) = 𝑉 )
21	17 20	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ⊥ ‘ { 𝑋 } ) = 𝑉 )
22	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ⊥ ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝐺 ) )
23	21 22	eqsstrrd	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → 𝑉 ⊆ ( 𝐿 ‘ 𝐺 ) )
24	15 23	eqssd	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
25	24	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ 𝑉 ) )
26	25	fveq2d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
27	12 26 24	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑋 = ( 0g ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
28	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) = 𝑉 )
29		simpr	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( 𝐿 ‘ 𝐺 ) = 𝑉 )
30	29	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ 𝑉 ) )
31	30	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ 𝑉 ) ) )
32	28 31 29	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
33	9	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
34		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
35	1 34 3 4 2	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
36	7 33 35	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
37	1 34 2	dochoc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ { 𝑋 } ) )
38	7 36 37	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ { 𝑋 } ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ { 𝑋 } ) )
40	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝐺 ) )
41		eqid	⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
42	1 3 7	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
43	42	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → 𝑈 ∈ LVec )
44	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
45	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → 𝑋 ∈ 𝑉 )
46		simprl	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → 𝑋 ≠ ( 0g ‘ 𝑈 ) )
47		eldifsn	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ ( 0g ‘ 𝑈 ) ) )
48	45 46 47	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → 𝑋 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
49	1 2 3 4 18 41 44 48	dochsnshp	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
50		simprr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 )
51	4 41 5 6 42 8	lkrshp4	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) ) )
53	50 52	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( 𝐿 ‘ 𝐺 ) ∈ ( LSHyp ‘ 𝑈 ) )
54	41 43 49 53	lshpcmp	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ( ⊥ ‘ { 𝑋 } ) ⊆ ( 𝐿 ‘ 𝐺 ) ↔ ( ⊥ ‘ { 𝑋 } ) = ( 𝐿 ‘ 𝐺 ) ) )
55	40 54	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ { 𝑋 } ) = ( 𝐿 ‘ 𝐺 ) )
56	55	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
57	56	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑋 } ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
58	39 57 55	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑋 ≠ ( 0g ‘ 𝑈 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
59	27 32 58	pm2.61da2ne	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )