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=BaseU
lcd0v.r ⊢R=Scalar⁡U
lcd0v.z ⊢0˙=0R
lcd0v.c ⊢C=LCDual⁡K⁡W
lcd0v.o ⊢O=0C
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=BaseU
4 lcd0v.r ⊢R=Scalar⁡U
5 lcd0v.z ⊢0˙=0R
6 lcd0v.c ⊢C=LCDual⁡K⁡W
7 lcd0v.o ⊢O=0C
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 ⊢φ→0C=0LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f
15 7 14 eqtrid ⊢φ→O=0LDual⁡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 ⊢0LDual⁡U=0LDual⁡U
23 eqid ⊢0LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f=0LDual⁡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→0LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f=0LDual⁡U
25 17 20 24 syl2anc ⊢φ→0LDual⁡U↾𝑠f∈LFnl⁡U|ocH⁡K⁡W⁡ocH⁡K⁡W⁡LKer⁡U⁡f=LKer⁡U⁡f=0LDual⁡U
26 3 4 5 12 22 16 ldual0v ⊢φ→0LDual⁡U=V×0˙
27 15 25 26 3eqtrd ⊢φ→O=V×0˙