Theorem lcdlss

Description: Subspaces of a dual vector space of functionals with closed kernels. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lcdlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdlss.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcdlss.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝐶 )
	lcdlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdlss.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcdlss.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcdlss.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcdlss.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
	lcdlss.b	⊢ 𝐵 = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcdlss.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcdlss	⊢ ( 𝜑 → 𝑆 = ( 𝑇 ∩ 𝒫 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		lcdlss.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdlss.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcdlss.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
4		lcdlss.s	⊢ 𝑆 = ( LSubSp ‘ 𝐶 )
5		lcdlss.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		lcdlss.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
7		lcdlss.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
8		lcdlss.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
9		lcdlss.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
10		lcdlss.b	⊢ 𝐵 = { 𝑓 ∈ 𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
11		lcdlss.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12	1 2 3 5 6 7 8 11 10	lcdval2	⊢ ( 𝜑 → 𝐶 = ( 𝐷 ↾s 𝐵 ) )
13	12	fveq2d	⊢ ( 𝜑 → ( LSubSp ‘ 𝐶 ) = ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) ) )
14	4 13	syl5eq	⊢ ( 𝜑 → 𝑆 = ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) ) )
15	14	eleq2d	⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↔ 𝑢 ∈ ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) ) ) )
16	1 5 11	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
17	8 16	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
18	1 5 2 6 7 8 9 10 11	lclkr	⊢ ( 𝜑 → 𝐵 ∈ 𝑇 )
19		eqid	⊢ ( 𝐷 ↾s 𝐵 ) = ( 𝐷 ↾s 𝐵 )
20		eqid	⊢ ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) ) = ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) )
21	19 9 20	lsslss	⊢ ( ( 𝐷 ∈ LMod ∧ 𝐵 ∈ 𝑇 ) → ( 𝑢 ∈ ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) ) ↔ ( 𝑢 ∈ 𝑇 ∧ 𝑢 ⊆ 𝐵 ) ) )
22	17 18 21	syl2anc	⊢ ( 𝜑 → ( 𝑢 ∈ ( LSubSp ‘ ( 𝐷 ↾s 𝐵 ) ) ↔ ( 𝑢 ∈ 𝑇 ∧ 𝑢 ⊆ 𝐵 ) ) )
23	15 22	bitrd	⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↔ ( 𝑢 ∈ 𝑇 ∧ 𝑢 ⊆ 𝐵 ) ) )
24		elin	⊢ ( 𝑢 ∈ ( 𝑇 ∩ 𝒫 𝐵 ) ↔ ( 𝑢 ∈ 𝑇 ∧ 𝑢 ∈ 𝒫 𝐵 ) )
25		velpw	⊢ ( 𝑢 ∈ 𝒫 𝐵 ↔ 𝑢 ⊆ 𝐵 )
26	25	anbi2i	⊢ ( ( 𝑢 ∈ 𝑇 ∧ 𝑢 ∈ 𝒫 𝐵 ) ↔ ( 𝑢 ∈ 𝑇 ∧ 𝑢 ⊆ 𝐵 ) )
27	24 26	bitr2i	⊢ ( ( 𝑢 ∈ 𝑇 ∧ 𝑢 ⊆ 𝐵 ) ↔ 𝑢 ∈ ( 𝑇 ∩ 𝒫 𝐵 ) )
28	23 27	bitrdi	⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 ↔ 𝑢 ∈ ( 𝑇 ∩ 𝒫 𝐵 ) ) )
29	28	eqrdv	⊢ ( 𝜑 → 𝑆 = ( 𝑇 ∩ 𝒫 𝐵 ) )