Theorem docavalN

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	docavalN	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq T\right)\to N\left(X\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)$$

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 5 6 7	docafvalN	$$⊢\left(K\in \mathrm{HL}\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)$$
9	8	adantr	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq T\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)$$
10	9	fveq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq T\right)\to N\left(X\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)\left(X\right)$$
11	5	fvexi	$$⊢T\in \mathrm{V}$$
12	11	elpw2	$$⊢X\in 𝒫T\leftrightarrow X\subseteq T$$
13	12	biimpri	$$⊢X\subseteq T\to X\in 𝒫T$$
14	13	adantl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq T\right)\to X\in 𝒫T$$
15		fvex	$$⊢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)\in \mathrm{V}$$
16		sseq1	$$⊢x=X\to \left(x\subseteq z\leftrightarrow X\subseteq z\right)$$
17	16	rabbidv	$$⊢x=X\to \left\{z\in \mathrm{ran}I|x\subseteq z\right\}=\left\{z\in \mathrm{ran}I|X\subseteq z\right\}$$
18	17	inteqd	$$⊢x=X\to \bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}=\bigcap \left\{z\in \mathrm{ran}I|X\subseteq z\right\}$$
19	18	fveq2d	$$⊢x=X\to I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|x\subseteq z\right\}\right)=I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|X\subseteq z\right\}\right)$$
20	19	fveq2d	$$⊢x=X\to \underset{\dot{}}{\perp }\left(I^{-1}\left(\bigcap \left\{z\in \mathrm{ran}I|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)$$
21	20	oveq1d	$$⊢x=X\to \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)=\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)$$
22	21	fvoveq1d	$$⊢x=X\to 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)=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)$$
23		eqid	$$⊢\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)=\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)$$
24	22 23	fvmptg	$$⊢\left(X\in 𝒫T\wedge 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)\in \mathrm{V}\right)\to \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)\left(X\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)$$
25	14 15 24	sylancl	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq T\right)\to \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)\left(X\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)$$
26	10 25	eqtrd	$$⊢\left(\left(K\in \mathrm{HL}\wedge W\in H\right)\wedge X\subseteq T\right)\to N\left(X\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)$$