Theorem lcdvadd

Description: Vector addition for the closed kernel vector space dual. (Contributed by NM, 10-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lcdvadd.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdvadd.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdvadd.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
4		lcdvadd.a	$$⊢\underset{\dot{}}{+}={+}_D$$
5		lcdvadd.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcdvadd.p	$$⊢\underset{\dot{}}{✚}={+}_C$$
7		lcdvadd.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 {+}_C={+}_{\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	ressplusg	$$⊢\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{}}{+}={+}_{\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{}}{+}={+}_{\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{}}{✚}=\underset{\dot{}}{+}$$