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