Theorem docafvalN

Description: Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	docaval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	docaval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	docaval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	docaval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	docaval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
	docaval.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
	docaval.n	$$⊢N=\mathrm{ocA}\left(K\right)\left(W\right)$$
Assertion	docafvalN	$$⊢\left(K\in V\wedge W\in H\right)\to N=\left(x\in 𝒫T⟼I\left(\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		docaval.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
2		docaval.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
3		docaval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
4		docaval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
5		docaval.t	$$⊢T=\mathrm{LTrn}\left(K\right)\left(W\right)$$
6		docaval.i	$$⊢I=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
7		docaval.n	$$⊢N=\mathrm{ocA}\left(K\right)\left(W\right)$$
8	1 2 3 4	docaffvalN	$$⊢K\in V\to \mathrm{ocA}\left(K\right)=\left(w\in H⟼\left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)$$
9	8	fveq1d	$$⊢K\in V\to \mathrm{ocA}\left(K\right)\left(W\right)=\left(w\in H⟼\left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\left(W\right)$$
10	7 9	eqtrid	$$⊢K\in V\to N=\left(w\in H⟼\left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\left(W\right)$$
11		fveq2	$$⊢w=W\to \mathrm{LTrn}\left(K\right)\left(w\right)=\mathrm{LTrn}\left(K\right)\left(W\right)$$
12	11 5	eqtr4di	$$⊢w=W\to \mathrm{LTrn}\left(K\right)\left(w\right)=T$$
13	12	pweqd	$$⊢w=W\to 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)=𝒫T$$
14		fveq2	$$⊢w=W\to \mathrm{DIsoA}\left(K\right)\left(w\right)=\mathrm{DIsoA}\left(K\right)\left(W\right)$$
15	14 6	eqtr4di	$$⊢w=W\to \mathrm{DIsoA}\left(K\right)\left(w\right)=I$$
16	15	cnveqd	$$⊢w=W\to {\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}=I^{-1}$$
17	15	rneqd	$$⊢w=W\to \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)=\mathrm{ran}I$$
18	17	rabeqdv	$$⊢w=W\to \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}=\left\{z\in \mathrm{ran}I|x\subseteq z\right\}$$
19	18	inteqd	$$⊢w=W\to \bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}=\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}$$
20	16 19	fveq12d	$$⊢w=W\to {\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)=I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)$$
21	20	fveq2d	$$⊢w=W\to \underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)=\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)$$
22		fveq2	$$⊢w=W\to \underset{\dot{}}{\perp }\left(w\right)=\underset{\dot{}}{\perp }\left(W\right)$$
23	21 22	oveq12d	$$⊢w=W\to \underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)=\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)$$
24		id	$$⊢w=W\to w=W$$
25	23 24	oveq12d	$$⊢w=W\to \left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w=\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W$$
26	15 25	fveq12d	$$⊢w=W\to \mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)=I\left(\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W\right)$$
27	13 26	mpteq12dv	$$⊢w=W\to \left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)=\left(x\in 𝒫T⟼I\left(\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
28		eqid	$$⊢\left(w\in H⟼\left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)=\left(w\in H⟼\left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)$$
29	5	fvexi	$$⊢T\in \mathrm{V}$$
30	29	pwex	$$⊢𝒫T\in \mathrm{V}$$
31	30	mptex	$$⊢\left(x\in 𝒫T⟼I\left(\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W\right)\right)\in \mathrm{V}$$
32	27 28 31	fvmpt	$$⊢W\in H\to \left(w\in H⟼\left(x\in 𝒫\mathrm{LTrn}\left(K\right)\left(w\right)⟼\mathrm{DIsoA}\left(K\right)\left(w\right)\left(\left(\underset{\dot{}}{\perp }\left({\mathrm{DIsoA}\left(K\right)\left(w\right)}^{-1}\left(\bigcap \left\{z\in \mathrm{ran}\mathrm{DIsoA}\left(K\right)\left(w\right)|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(w\right)\right)\underset{\dot{}}{\wedge }w\right)\right)\right)\left(W\right)=\left(x\in 𝒫T⟼I\left(\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$
33	10 32	sylan9eq	$$⊢\left(K\in V\wedge W\in H\right)\to N=\left(x\in 𝒫T⟼I\left(\left(\underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)\right)\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(W\right)\right)\underset{\dot{}}{\wedge }W\right)\right)$$