Metamath Proof Explorer


Theorem lcdlsp

Description: Span in the set of functionals with closed kernels. (Contributed by NM, 28-Mar-2015)

Ref Expression
Hypotheses lcdlsp.h H = LHyp K
lcdlsp.u U = DVecH K W
lcdlsp.d D = LDual U
lcdlsp.m M = LSpan D
lcdlsp.c C = LCDual K W
lcdlsp.f F = Base C
lcdlsp.n N = LSpan C
lcdlsp.k φ K HL W H
lcdlsp.g φ G F
Assertion lcdlsp φ N G = M G

Proof

Step Hyp Ref Expression
1 lcdlsp.h H = LHyp K
2 lcdlsp.u U = DVecH K W
3 lcdlsp.d D = LDual U
4 lcdlsp.m M = LSpan D
5 lcdlsp.c C = LCDual K W
6 lcdlsp.f F = Base C
7 lcdlsp.n N = LSpan C
8 lcdlsp.k φ K HL W H
9 lcdlsp.g φ G F
10 eqid ocH K W = ocH K W
11 eqid LFnl U = LFnl U
12 eqid LKer U = LKer U
13 1 10 5 2 11 12 3 8 lcdval φ C = D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f
14 13 fveq2d φ LSpan C = LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f
15 7 14 syl5eq φ N = LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f
16 15 fveq1d φ N G = LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f G
17 1 2 8 dvhlmod φ U LMod
18 3 17 lduallmod φ D LMod
19 eqid LSubSp D = LSubSp D
20 eqid f LFnl U | ocH K W ocH K W LKer U f = LKer U f = f LFnl U | ocH K W ocH K W LKer U f = LKer U f
21 1 2 10 11 12 3 19 20 8 lclkr φ f LFnl U | ocH K W ocH K W LKer U f = LKer U f LSubSp D
22 1 10 5 6 2 11 12 20 8 lcdvbase φ F = f LFnl U | ocH K W ocH K W LKer U f = LKer U f
23 9 22 sseqtrd φ G f LFnl U | ocH K W ocH K W LKer U f = LKer U f
24 eqid D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f = D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f
25 eqid LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f = LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f
26 24 4 25 19 lsslsp D LMod f LFnl U | ocH K W ocH K W LKer U f = LKer U f LSubSp D G f LFnl U | ocH K W ocH K W LKer U f = LKer U f M G = LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f G
27 18 21 23 26 syl3anc φ M G = LSpan D 𝑠 f LFnl U | ocH K W ocH K W LKer U f = LKer U f G
28 16 27 eqtr4d φ N G = M G