Theorem lcdvs

Description: Scalar product for the closed kernel vector space dual. (Contributed by NM, 28-Mar-2015)

	Ref	Expression
Hypotheses	lcdvs.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdvs.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdvs.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcdvs.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lcdvs.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdvs.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	lcdvs.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcdvs	$$⊢\phi \to \underset{\dot{}}{\bullet }=\underset{\dot{}}{·}$$

Proof

Step	Hyp	Ref	Expression
1		lcdvs.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvs.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvs.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
4		lcdvs.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
5		lcdvs.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcdvs.m	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
7		lcdvs.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
9		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
10		eqid	$$⊢\mathrm{LKer}\left(U\right)=\mathrm{LKer}\left(U\right)$$
11	1 8 5 2 9 10 3 7	lcdval	$$⊢\phi \to C=D{\upharpoonright }_{𝑠}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}$$
12	11	fveq2d	$$⊢\phi \to {\cdot }_C={\cdot }_{\left(D{\upharpoonright }_{𝑠}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\right)}$$
13		fvex	$$⊢\mathrm{LFnl}\left(U\right)\in \mathrm{V}$$
14	13	rabex	$$⊢\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\in \mathrm{V}$$
15		eqid	$$⊢D{\upharpoonright }_{𝑠}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}=D{\upharpoonright }_{𝑠}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}$$
16	15 4	ressvsca	$$⊢\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\in \mathrm{V}\to \underset{\dot{}}{·}={\cdot }_{\left(D{\upharpoonright }_{𝑠}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\right)}$$
17	14 16	ax-mp	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(D{\upharpoonright }_{𝑠}\left\{f\in \mathrm{LFnl}\left(U\right)|\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{ocH}\left(K\right)\left(W\right)\left(\mathrm{LKer}\left(U\right)\left(f\right)\right)\right)=\mathrm{LKer}\left(U\right)\left(f\right)\right\}\right)}$$
18	12 6 17	3eqtr4g	$$⊢\phi \to \underset{\dot{}}{\bullet }=\underset{\dot{}}{·}$$