Theorem ocvfval

Description: The orthocomplement operation. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	ocvfval.v	$$⊢V={\mathrm{Base}}_W$$
	ocvfval.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	ocvfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	ocvfval.z	$$⊢\underset{\dot{}}{0}=0_F$$
	ocvfval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
Assertion	ocvfval	$$⊢W\in X\to \underset{\dot{}}{\perp }=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ocvfval.v	$$⊢V={\mathrm{Base}}_W$$
2		ocvfval.i	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		ocvfval.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		ocvfval.z	$$⊢\underset{\dot{}}{0}=0_F$$
5		ocvfval.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
6		elex	$$⊢W\in X\to W\in \mathrm{V}$$
7		fveq2	$$⊢h=W\to {\mathrm{Base}}_h={\mathrm{Base}}_W$$
8	7 1	eqtr4di	$$⊢h=W\to {\mathrm{Base}}_h=V$$
9	8	pweqd	$$⊢h=W\to 𝒫{\mathrm{Base}}_h=𝒫V$$
10		fveq2	$$⊢h=W\to {\cdot }_{𝑖}\left(h\right)={\cdot }_{𝑖}\left(W\right)$$
11	10 2	eqtr4di	$$⊢h=W\to {\cdot }_{𝑖}\left(h\right)=\underset{\dot{}}{,}$$
12	11	oveqd	$$⊢h=W\to x{\cdot }_{𝑖}\left(h\right)y=x\underset{\dot{}}{,}y$$
13		fveq2	$$⊢h=W\to \mathrm{Scalar}\left(h\right)=\mathrm{Scalar}\left(W\right)$$
14	13 3	eqtr4di	$$⊢h=W\to \mathrm{Scalar}\left(h\right)=F$$
15	14	fveq2d	$$⊢h=W\to 0_{\mathrm{Scalar}\left(h\right)}=0_F$$
16	15 4	eqtr4di	$$⊢h=W\to 0_{\mathrm{Scalar}\left(h\right)}=\underset{\dot{}}{0}$$
17	12 16	eqeq12d	$$⊢h=W\to \left(x{\cdot }_{𝑖}\left(h\right)y=0_{\mathrm{Scalar}\left(h\right)}\leftrightarrow x\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right)$$
18	17	ralbidv	$$⊢h=W\to \left(\forall y\in sx{\cdot }_{𝑖}\left(h\right)y=0_{\mathrm{Scalar}\left(h\right)}\leftrightarrow \forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right)$$
19	8 18	rabeqbidv	$$⊢h=W\to \left\{x\in {\mathrm{Base}}_h|\forall y\in sx{\cdot }_{𝑖}\left(h\right)y=0_{\mathrm{Scalar}\left(h\right)}\right\}=\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
20	9 19	mpteq12dv	$$⊢h=W\to \left(s\in 𝒫{\mathrm{Base}}_h⟼\left\{x\in {\mathrm{Base}}_h|\forall y\in sx{\cdot }_{𝑖}\left(h\right)y=0_{\mathrm{Scalar}\left(h\right)}\right\}\right)=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$
21		df-ocv	$$⊢\mathrm{ocv}=\left(h\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_h⟼\left\{x\in {\mathrm{Base}}_h|\forall y\in sx{\cdot }_{𝑖}\left(h\right)y=0_{\mathrm{Scalar}\left(h\right)}\right\}\right)\right)$$
22		eqid	$$⊢\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$
23	1	fvexi	$$⊢V\in \mathrm{V}$$
24		ssrab2	$$⊢\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\subseteq V$$
25	23 24	elpwi2	$$⊢\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\in 𝒫V$$
26	25	a1i	$$⊢s\in 𝒫V\to \left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\in 𝒫V$$
27	22 26	fmpti	$$⊢\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right):𝒫V⟶𝒫V$$
28	23	pwex	$$⊢𝒫V\in \mathrm{V}$$
29		fex2	$$⊢\left(\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right):𝒫V⟶𝒫V\wedge 𝒫V\in \mathrm{V}\wedge 𝒫V\in \mathrm{V}\right)\to \left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)\in \mathrm{V}$$
30	27 28 28 29	mp3an	$$⊢\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)\in \mathrm{V}$$
31	20 21 30	fvmpt	$$⊢W\in \mathrm{V}\to \mathrm{ocv}\left(W\right)=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$
32	6 31	syl	$$⊢W\in X\to \mathrm{ocv}\left(W\right)=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$
33	5 32	syl5eq	$$⊢W\in X\to \underset{\dot{}}{\perp }=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$