Theorem lcdlss2N

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

	Ref	Expression
Hypotheses	lcdlss2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcdlss2.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
	lcdlss2.s	⊢ 𝑆 = ( LSubSp ‘ 𝐶 )
	lcdlss2.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
	lcdlss2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcdlss2.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcdlss2.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
	lcdlss2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcdlss2N	⊢ ( 𝜑 → 𝑆 = ( 𝑇 ∩ 𝒫 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		lcdlss2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcdlss2.c	⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
3		lcdlss2.s	⊢ 𝑆 = ( LSubSp ‘ 𝐶 )
4		lcdlss2.v	⊢ 𝑉 = ( Base ‘ 𝐶 )
5		lcdlss2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		lcdlss2.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
7		lcdlss2.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
8		lcdlss2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9		eqid	⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
10		eqid	⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
11		eqid	⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
12		eqid	⊢ { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) }
13	1 9 2 3 5 10 11 6 7 12 8	lcdlss	⊢ ( 𝜑 → 𝑆 = ( 𝑇 ∩ 𝒫 { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
14	1 9 2 4 5 10 11 12 8	lcdvbase	⊢ ( 𝜑 → 𝑉 = { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
15	14	pweqd	⊢ ( 𝜑 → 𝒫 𝑉 = 𝒫 { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } )
16	15	ineq2d	⊢ ( 𝜑 → ( 𝑇 ∩ 𝒫 𝑉 ) = ( 𝑇 ∩ 𝒫 { 𝑓 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑓 ) } ) )
17	13 16	eqtr4d	⊢ ( 𝜑 → 𝑆 = ( 𝑇 ∩ 𝒫 𝑉 ) )