Metamath Proof Explorer

Theorem lcdfval

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

Ref Expression
Hypothesis lcdval.h ⊢ H = LHyp ⁡ K
Assertion 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

Proof

Step Hyp Ref Expression
1 lcdval.h ⊢ H = LHyp ⁡ K
2 elex ⊢ K ∈ X → K ∈ V
3 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
4 3 1 eqtr4di ⊢ k = K → LHyp ⁡ k = H
5 fveq2 ⊢ k = K → DVecH ⁡ k = DVecH ⁡ K
6 5 fveq1d ⊢ k = K → DVecH ⁡ k ⁡ w = DVecH ⁡ K ⁡ w
7 6 fveq2d ⊢ k = K → LDual ⁡ DVecH ⁡ k ⁡ w = LDual ⁡ DVecH ⁡ K ⁡ w
8 6 fveq2d ⊢ k = K → LFnl ⁡ DVecH ⁡ k ⁡ w = LFnl ⁡ DVecH ⁡ K ⁡ w
9 fveq2 ⊢ k = K → ocH ⁡ k = ocH ⁡ K
10 9 fveq1d ⊢ k = K → ocH ⁡ k ⁡ w = ocH ⁡ K ⁡ w
11 6 fveq2d ⊢ k = K → LKer ⁡ DVecH ⁡ k ⁡ w = LKer ⁡ DVecH ⁡ K ⁡ w
12 11 fveq1d ⊢ k = K → LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f
13 10 12 fveq12d ⊢ k = K → ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = ocH ⁡ K ⁡ w ⁡ LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f
14 10 13 fveq12d ⊢ k = K → ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = ocH ⁡ K ⁡ w ⁡ ocH ⁡ K ⁡ w ⁡ LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f
15 14 12 eqeq12d ⊢ k = K → ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f ↔ ocH ⁡ K ⁡ w ⁡ ocH ⁡ K ⁡ w ⁡ LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f
16 8 15 rabeqbidv ⊢ k = K → f ∈ LFnl ⁡ DVecH ⁡ k ⁡ w | ocH ⁡ k ⁡ w ⁡ ocH ⁡ k ⁡ w ⁡ LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ k ⁡ w ⁡ f = f ∈ LFnl ⁡ DVecH ⁡ K ⁡ w | ocH ⁡ K ⁡ w ⁡ ocH ⁡ K ⁡ w ⁡ LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f = LKer ⁡ DVecH ⁡ K ⁡ w ⁡ f
17 7 16 oveq12d ⊢ k = K → 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 = 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
18 4 17 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ 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
19 df-lcdual ⊢ LCDual = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ 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
20 18 19 1 mptfvmpt ⊢ K ∈ V → 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
21 2 20 syl ⊢ 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