Metamath Proof Explorer

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 ⊢H=LHyp⁡K
lclkrs2.o ⊢⊥˙=ocH⁡K⁡W
lclkrs2.u ⊢U=DVecH⁡K⁡W
lclkrs2.s ⊢S=LSubSp⁡U
lclkrs2.f ⊢F=LFnl⁡U
lclkrs2.l ⊢L=LKer⁡U
lclkrs2.d ⊢D=LDual⁡U
lclkrs2.t ⊢T=LSubSp⁡D
lclkrs2.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
lclkrs2.r ⊢R=g∈F|⊥˙⁡⊥˙⁡L⁡g=L⁡g∧⊥˙⁡L⁡g⊆Q
lclkrs2.k ⊢φ→K∈HL∧W∈H
lclkrs2.q ⊢φ→Q∈S
Assertion lclkrs2 ⊢φ→R∈T∧R⊆C

Proof

Step Hyp Ref Expression
1 lclkrs2.h ⊢H=LHyp⁡K
2 lclkrs2.o ⊢⊥˙=ocH⁡K⁡W
3 lclkrs2.u ⊢U=DVecH⁡K⁡W
4 lclkrs2.s ⊢S=LSubSp⁡U
5 lclkrs2.f ⊢F=LFnl⁡U
6 lclkrs2.l ⊢L=LKer⁡U
7 lclkrs2.d ⊢D=LDual⁡U
8 lclkrs2.t ⊢T=LSubSp⁡D
9 lclkrs2.c ⊢C=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
10 lclkrs2.r ⊢R=g∈F|⊥˙⁡⊥˙⁡L⁡g=L⁡g∧⊥˙⁡L⁡g⊆Q
11 lclkrs2.k ⊢φ→K∈HL∧W∈H
12 lclkrs2.q ⊢φ→Q∈S
13 1 2 3 4 5 6 7 8 10 11 12 lclkrs ⊢φ→R∈T
14 simpl ⊢⊥˙⁡⊥˙⁡L⁡g=L⁡g∧⊥˙⁡L⁡g⊆Q→⊥˙⁡⊥˙⁡L⁡g=L⁡g
15 14 a1i ⊢g∈F→⊥˙⁡⊥˙⁡L⁡g=L⁡g∧⊥˙⁡L⁡g⊆Q→⊥˙⁡⊥˙⁡L⁡g=L⁡g
16 15 ss2rabi ⊢g∈F|⊥˙⁡⊥˙⁡L⁡g=L⁡g∧⊥˙⁡L⁡g⊆Q⊆g∈F|⊥˙⁡⊥˙⁡L⁡g=L⁡g
17 fveq2 ⊢f=g→L⁡f=L⁡g
18 17 fveq2d ⊢f=g→⊥˙⁡L⁡f=⊥˙⁡L⁡g
19 18 fveq2d ⊢f=g→⊥˙⁡⊥˙⁡L⁡f=⊥˙⁡⊥˙⁡L⁡g
20 19 17 eqeq12d ⊢f=g→⊥˙⁡⊥˙⁡L⁡f=L⁡f↔⊥˙⁡⊥˙⁡L⁡g=L⁡g
21 20 cbvrabv ⊢f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f=g∈F|⊥˙⁡⊥˙⁡L⁡g=L⁡g
22 9 21 eqtri ⊢C=g∈F|⊥˙⁡⊥˙⁡L⁡g=L⁡g
23 16 10 22 3sstr4i ⊢R⊆C
24 13 23 jctir ⊢φ→R∈T∧R⊆C