Theorem lclkrs2

Description: The set of functionals with closed kernels and majorizing the orthocomplement of a given subspace Q is a subspace of the dual space containing functionals with closed kernels. Note that R is the value given by mapdval . (Contributed by NM, 12-Mar-2015)

	Ref	Expression
Hypotheses	lclkrs2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lclkrs2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrs2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lclkrs2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	lclkrs2.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lclkrs2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lclkrs2.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lclkrs2.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
	lclkrs2.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lclkrs2.r	⊢ 𝑅 = { 𝑔 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑄 ) }
	lclkrs2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lclkrs2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
Assertion	lclkrs2	⊢ ( 𝜑 → ( 𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		lclkrs2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lclkrs2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lclkrs2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lclkrs2.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5		lclkrs2.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
6		lclkrs2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
7		lclkrs2.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
8		lclkrs2.t	⊢ 𝑇 = ( LSubSp ‘ 𝐷 )
9		lclkrs2.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
10		lclkrs2.r	⊢ 𝑅 = { 𝑔 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑄 ) }
11		lclkrs2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		lclkrs2.q	⊢ ( 𝜑 → 𝑄 ∈ 𝑆 )
13	1 2 3 4 5 6 7 8 10 11 12	lclkrs	⊢ ( 𝜑 → 𝑅 ∈ 𝑇 )
14		simpl	⊢ ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑄 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) )
15	14	a1i	⊢ ( 𝑔 ∈ 𝐹 → ( ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑄 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ) )
16	15	ss2rabi	⊢ { 𝑔 ∈ 𝐹 ∣ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑄 ) } ⊆ { 𝑔 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
17		fveq2	⊢ ( 𝑓 = 𝑔 → ( 𝐿 ‘ 𝑓 ) = ( 𝐿 ‘ 𝑔 ) )
18	17	fveq2d	⊢ ( 𝑓 = 𝑔 → ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) = ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
19	18	fveq2d	⊢ ( 𝑓 = 𝑔 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) )
20	19 17	eqeq12d	⊢ ( 𝑓 = 𝑔 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ) )
21	20	cbvrabv	⊢ { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) } = { 𝑔 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
22	9 21	eqtri	⊢ 𝐶 = { 𝑔 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) }
23	16 10 22	3sstr4i	⊢ 𝑅 ⊆ 𝐶
24	13 23	jctir	⊢ ( 𝜑 → ( 𝑅 ∈ 𝑇 ∧ 𝑅 ⊆ 𝐶 ) )