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 eqtrid ⊢ φ → 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