Metamath Proof Explorer

Theorem lcd0v

Description: The zero functional in the set of functionals with closed kernels. (Contributed by NM, 20-Mar-2015)

Ref Expression
Hypotheses lcd0v.h ⊢ H = LHyp ⁡ K
lcd0v.u ⊢ U = DVecH ⁡ K ⁡ W
lcd0v.v ⊢ V = Base U
lcd0v.r ⊢ R = Scalar ⁡ U
lcd0v.z ⊢ 0 ˙ = 0 R
lcd0v.c ⊢ C = LCDual ⁡ K ⁡ W
lcd0v.o ⊢ O = 0 C
lcd0v.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion lcd0v ⊢ φ → O = V × 0 ˙

Proof

Step Hyp Ref Expression
1 lcd0v.h ⊢ H = LHyp ⁡ K
2 lcd0v.u ⊢ U = DVecH ⁡ K ⁡ W
3 lcd0v.v ⊢ V = Base U
4 lcd0v.r ⊢ R = Scalar ⁡ U
5 lcd0v.z ⊢ 0 ˙ = 0 R
6 lcd0v.c ⊢ C = LCDual ⁡ K ⁡ W
7 lcd0v.o ⊢ O = 0 C
8 lcd0v.k ⊢ φ → K ∈ HL ∧ W ∈ H
9 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
10 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
11 eqid ⊢ LKer ⁡ U = LKer ⁡ U
12 eqid ⊢ LDual ⁡ U = LDual ⁡ U
13 1 9 6 2 10 11 12 8 lcdval ⊢ φ → C = LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
14 13 fveq2d ⊢ φ → 0 C = 0 LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
15 7 14 syl5eq ⊢ φ → O = 0 LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
16 1 2 8 dvhlmod ⊢ φ → U ∈ LMod
17 12 16 lduallmod ⊢ φ → LDual ⁡ U ∈ LMod
18 eqid ⊢ LSubSp ⁡ LDual ⁡ U = LSubSp ⁡ LDual ⁡ U
19 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
20 1 2 9 10 11 12 18 19 8 lclkr ⊢ φ → f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∈ LSubSp ⁡ LDual ⁡ U
21 eqid ⊢ LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
22 eqid ⊢ 0 LDual ⁡ U = 0 LDual ⁡ U
23 eqid ⊢ 0 LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = 0 LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f
24 21 22 23 18 lss0v ⊢ LDual ⁡ U ∈ LMod ∧ f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f ∈ LSubSp ⁡ LDual ⁡ U → 0 LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = 0 LDual ⁡ U
25 17 20 24 syl2anc ⊢ φ → 0 LDual ⁡ U ↾ 𝑠 f ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ f = LKer ⁡ U ⁡ f = 0 LDual ⁡ U
26 3 4 5 12 22 16 ldual0v ⊢ φ → 0 LDual ⁡ U = V × 0 ˙
27 15 25 26 3eqtrd ⊢ φ → O = V × 0 ˙