Theorem dochfval

Description: Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014)

	Ref	Expression
Hypotheses	dochval.b	$$⊢B={\mathrm{Base}}_K$$
	dochval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
	dochval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	dochval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	dochval.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
	dochval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	dochval.v	$$⊢V={\mathrm{Base}}_U$$
	dochval.n	$$⊢N=\mathrm{ocH}\left(K\right)\left(W\right)$$
Assertion	dochfval	$$⊢\left(K\in X\wedge W\in H\right)\to N=\left(x\in 𝒫V⟼I\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dochval.b	$$⊢B={\mathrm{Base}}_K$$
2		dochval.g	$$⊢G=\mathrm{glb}\left(K\right)$$
3		dochval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
4		dochval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		dochval.i	$$⊢I=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
6		dochval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
7		dochval.v	$$⊢V={\mathrm{Base}}_U$$
8		dochval.n	$$⊢N=\mathrm{ocH}\left(K\right)\left(W\right)$$
9	1 2 3 4	dochffval	$$⊢K\in X\to \mathrm{ocH}\left(K\right)=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)\right)$$
10	9	fveq1d	$$⊢K\in X\to \mathrm{ocH}\left(K\right)\left(W\right)=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)\right)\left(W\right)$$
11	8 10	syl5eq	$$⊢K\in X\to N=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)\right)\left(W\right)$$
12		fveq2	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(W\right)$$
13	12 6	eqtr4di	$$⊢w=W\to \mathrm{DVecH}\left(K\right)\left(w\right)=U$$
14	13	fveq2d	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}={\mathrm{Base}}_U$$
15	14 7	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}=V$$
16	15	pweqd	$$⊢w=W\to 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}=𝒫V$$
17		fveq2	$$⊢w=W\to \mathrm{DIsoH}\left(K\right)\left(w\right)=\mathrm{DIsoH}\left(K\right)\left(W\right)$$
18	17 5	eqtr4di	$$⊢w=W\to \mathrm{DIsoH}\left(K\right)\left(w\right)=I$$
19	18	fveq1d	$$⊢w=W\to \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)=I\left(y\right)$$
20	19	sseq2d	$$⊢w=W\to \left(x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\leftrightarrow x\subseteq I\left(y\right)\right)$$
21	20	rabbidv	$$⊢w=W\to \left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}=\left\{y\in B|x\subseteq I\left(y\right)\right\}$$
22	21	fveq2d	$$⊢w=W\to G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)=G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)$$
23	22	fveq2d	$$⊢w=W\to \underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)=\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)$$
24	18 23	fveq12d	$$⊢w=W\to \mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)=I\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)\right)$$
25	16 24	mpteq12dv	$$⊢w=W\to \left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)=\left(x\in 𝒫V⟼I\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)\right)\right)$$
26		eqid	$$⊢\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)\right)=\left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)\right)$$
27	7	fvexi	$$⊢V\in \mathrm{V}$$
28	27	pwex	$$⊢𝒫V\in \mathrm{V}$$
29	28	mptex	$$⊢\left(x\in 𝒫V⟼I\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)\right)\right)\in \mathrm{V}$$
30	25 26 29	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left(x\in 𝒫{\mathrm{Base}}_{\mathrm{DVecH}\left(K\right)\left(w\right)}⟼\mathrm{DIsoH}\left(K\right)\left(w\right)\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq \mathrm{DIsoH}\left(K\right)\left(w\right)\left(y\right)\right\}\right)\right)\right)\right)\right)\left(W\right)=\left(x\in 𝒫V⟼I\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)\right)\right)$$
31	11 30	sylan9eq	$$⊢\left(K\in X\wedge W\in H\right)\to N=\left(x\in 𝒫V⟼I\left(\underset{\dot{}}{\perp }\left(G\left(\left\{y\in B|x\subseteq I\left(y\right)\right\}\right)\right)\right)\right)$$