Metamath Proof Explorer

Theorem lcdval

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

Ref Expression
Hypotheses lcdval.h ⊢H=LHyp⁡K
lcdval.o ⊢⊥˙=ocH⁡K⁡W
lcdval.c ⊢C=LCDual⁡K⁡W
lcdval.u ⊢U=DVecH⁡K⁡W
lcdval.f ⊢F=LFnl⁡U
lcdval.l ⊢L=LKer⁡U
lcdval.d ⊢D=LDual⁡U
lcdval.k ⊢φ→K∈X∧W∈H
Assertion lcdval ⊢φ→C=D↾𝑠f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f

Proof

Step Hyp Ref Expression
1 lcdval.h ⊢H=LHyp⁡K
2 lcdval.o ⊢⊥˙=ocH⁡K⁡W
3 lcdval.c ⊢C=LCDual⁡K⁡W
4 lcdval.u ⊢U=DVecH⁡K⁡W
5 lcdval.f ⊢F=LFnl⁡U
6 lcdval.l ⊢L=LKer⁡U
7 lcdval.d ⊢D=LDual⁡U
8 lcdval.k ⊢φ→K∈X∧W∈H
9 1 lcdfval ⊢K∈X→LCDual⁡K=w∈H⟼LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f
10 9 fveq1d ⊢K∈X→LCDual⁡K⁡W=w∈H⟼LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f⁡W
11 3 10 eqtrid ⊢K∈X→C=w∈H⟼LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f⁡W
12 fveq2 ⊢w=W→DVecH⁡K⁡w=DVecH⁡K⁡W
13 12 4 eqtr4di ⊢w=W→DVecH⁡K⁡w=U
14 13 fveq2d ⊢w=W→LDual⁡DVecH⁡K⁡w=LDual⁡U
15 14 7 eqtr4di ⊢w=W→LDual⁡DVecH⁡K⁡w=D
16 13 fveq2d ⊢w=W→LFnl⁡DVecH⁡K⁡w=LFnl⁡U
17 16 5 eqtr4di ⊢w=W→LFnl⁡DVecH⁡K⁡w=F
18 fveq2 ⊢w=W→ocH⁡K⁡w=ocH⁡K⁡W
19 18 2 eqtr4di ⊢w=W→ocH⁡K⁡w=⊥˙
20 13 fveq2d ⊢w=W→LKer⁡DVecH⁡K⁡w=LKer⁡U
21 20 6 eqtr4di ⊢w=W→LKer⁡DVecH⁡K⁡w=L
22 21 fveq1d ⊢w=W→LKer⁡DVecH⁡K⁡w⁡f=L⁡f
23 19 22 fveq12d ⊢w=W→ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=⊥˙⁡L⁡f
24 19 23 fveq12d ⊢w=W→ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=⊥˙⁡⊥˙⁡L⁡f
25 24 22 eqeq12d ⊢w=W→ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f↔⊥˙⁡⊥˙⁡L⁡f=L⁡f
26 17 25 rabeqbidv ⊢w=W→f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f=f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
27 15 26 oveq12d ⊢w=W→LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f=D↾𝑠f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
28 eqid ⊢w∈H⟼LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f=w∈H⟼LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f
29 ovex ⊢D↾𝑠f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f∈V
30 27 28 29 fvmpt ⊢W∈H→w∈H⟼LDual⁡DVecH⁡K⁡w↾𝑠f∈LFnl⁡DVecH⁡K⁡w|ocH⁡K⁡w⁡ocH⁡K⁡w⁡LKer⁡DVecH⁡K⁡w⁡f=LKer⁡DVecH⁡K⁡w⁡f⁡W=D↾𝑠f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
31 11 30 sylan9eq ⊢K∈X∧W∈H→C=D↾𝑠f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f
32 8 31 syl ⊢φ→C=D↾𝑠f∈F|⊥˙⁡⊥˙⁡L⁡f=L⁡f