Theorem ocvval

Description: Value of the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (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	ocvval	$$⊢S\subseteq V\to \underset{\dot{}}{\perp }\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\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	1	fvexi	$$⊢V\in \mathrm{V}$$
7	6	elpw2	$$⊢S\in 𝒫V\leftrightarrow S\subseteq V$$
8	1 2 3 4 5	ocvfval	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)$$
9	8	fveq1d	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\perp }\left(S\right)=\left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)\left(S\right)$$
10		raleq	$$⊢s=S\to \left(\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\leftrightarrow \forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right)$$
11	10	rabbidv	$$⊢s=S\to \left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
12		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)$$
13	6	rabex	$$⊢\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
14	11 12 13	fvmpt	$$⊢S\in 𝒫V\to \left(s\in 𝒫V⟼\left\{x\in V|\forall y\in sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\right)\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
15	9 14	sylan9eq	$$⊢\left(W\in \mathrm{V}\wedge S\in 𝒫V\right)\to \underset{\dot{}}{\perp }\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
16		0fv	$$⊢\varnothing \left(S\right)=\varnothing$$
17		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{ocv}\left(W\right)=\varnothing$$
18	5 17	syl5eq	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\varnothing$$
19	18	fveq1d	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }\left(S\right)=\varnothing \left(S\right)$$
20		ssrab2	$$⊢\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\subseteq V$$
21		fvprc	$$⊢\neg W\in \mathrm{V}\to {\mathrm{Base}}_W=\varnothing$$
22	1 21	syl5eq	$$⊢\neg W\in \mathrm{V}\to V=\varnothing$$
23		sseq0	$$⊢\left(\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}\subseteq V\wedge V=\varnothing \right)\to \left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}=\varnothing$$
24	20 22 23	sylancr	$$⊢\neg W\in \mathrm{V}\to \left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}=\varnothing$$
25	16 19 24	3eqtr4a	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
26	25	adantr	$$⊢\left(\neg W\in \mathrm{V}\wedge S\in 𝒫V\right)\to \underset{\dot{}}{\perp }\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
27	15 26	pm2.61ian	$$⊢S\in 𝒫V\to \underset{\dot{}}{\perp }\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$
28	7 27	sylbir	$$⊢S\subseteq V\to \underset{\dot{}}{\perp }\left(S\right)=\left\{x\in V|\forall y\in Sx\underset{\dot{}}{,}y=\underset{\dot{}}{0}\right\}$$