Theorem lcd0v2

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

	Ref	Expression
Hypotheses	lcd0v2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcd0v2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcd0v2.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcd0v2.z	$$⊢\underset{\dot{}}{0}=0_D$$
	lcd0v2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcd0v2.o	$$⊢O=0_C$$
	lcd0v2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcd0v2	$$⊢\phi \to O=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		lcd0v2.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcd0v2.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcd0v2.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
4		lcd0v2.z	$$⊢\underset{\dot{}}{0}=0_D$$
5		lcd0v2.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcd0v2.o	$$⊢O=0_C$$
7		lcd0v2.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		eqid	$$⊢{\mathrm{Base}}_U={\mathrm{Base}}_U$$
9		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
10		eqid	$$⊢0_{\mathrm{Scalar}\left(U\right)}=0_{\mathrm{Scalar}\left(U\right)}$$
11	1 2 8 9 10 5 6 7	lcd0v	$$⊢\phi \to O={\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}$$
12	1 2 7	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
13	8 9 10 3 4 12	ldual0v	$$⊢\phi \to \underset{\dot{}}{0}={\mathrm{Base}}_U\times \left\{0_{\mathrm{Scalar}\left(U\right)}\right\}$$
14	11 13	eqtr4d	$$⊢\phi \to O=\underset{\dot{}}{0}$$