Theorem elocv

Description: Elementhood in the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed 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	elocv	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\leftrightarrow \left(S\subseteq V\wedge A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\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		elfvdm	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to S\in \mathrm{dom}\underset{\dot{}}{\perp }$$
7		n0i	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to \neg \underset{\dot{}}{\perp }\left(S\right)=\varnothing$$
8		fvprc	$$⊢\neg W\in \mathrm{V}\to \mathrm{ocv}\left(W\right)=\varnothing$$
9	5 8	syl5eq	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\varnothing$$
10	9	fveq1d	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }\left(S\right)=\varnothing \left(S\right)$$
11		0fv	$$⊢\varnothing \left(S\right)=\varnothing$$
12	10 11	syl6eq	$$⊢\neg W\in \mathrm{V}\to \underset{\dot{}}{\perp }\left(S\right)=\varnothing$$
13	7 12	nsyl2	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to W\in \mathrm{V}$$
14	1 2 3 4 5	ocvfval	$$⊢W\in \mathrm{V}\to \underset{\dot{}}{\perp }=\left(s\in 𝒫V⟼\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)$$
15	13 14	syl	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to \underset{\dot{}}{\perp }=\left(s\in 𝒫V⟼\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)$$
16	15	dmeqd	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to \mathrm{dom}\underset{\dot{}}{\perp }=\mathrm{dom}\left(s\in 𝒫V⟼\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)$$
17	1	fvexi	$$⊢V\in \mathrm{V}$$
18	17	rabex	$$⊢\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
19		eqid	$$⊢\left(s\in 𝒫V⟼\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)=\left(s\in 𝒫V⟼\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)$$
20	18 19	dmmpti	$$⊢\mathrm{dom}\left(s\in 𝒫V⟼\left\{y\in V|\forall x\in sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)=𝒫V$$
21	16 20	syl6eq	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to \mathrm{dom}\underset{\dot{}}{\perp }=𝒫V$$
22	6 21	eleqtrd	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to S\in 𝒫V$$
23	22	elpwid	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\to S\subseteq V$$
24	1 2 3 4 5	ocvval	$$⊢S\subseteq V\to \underset{\dot{}}{\perp }\left(S\right)=\left\{y\in V|\forall x\in Sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}$$
25	24	eleq2d	$$⊢S\subseteq V\to \left(A\in \underset{\dot{}}{\perp }\left(S\right)\leftrightarrow A\in \left\{y\in V|\forall x\in Sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\right)$$
26		oveq1	$$⊢y=A\to y\underset{\dot{}}{,}x=A\underset{\dot{}}{,}x$$
27	26	eqeq1d	$$⊢y=A\to \left(y\underset{\dot{}}{,}x=\underset{\dot{}}{0}\leftrightarrow A\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)$$
28	27	ralbidv	$$⊢y=A\to \left(\forall x\in Sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\leftrightarrow \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)$$
29	28	elrab	$$⊢A\in \left\{y\in V|\forall x\in Sy\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right\}\leftrightarrow \left(A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)$$
30	25 29	syl6bb	$$⊢S\subseteq V\to \left(A\in \underset{\dot{}}{\perp }\left(S\right)\leftrightarrow \left(A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)\right)$$
31	23 30	biadanii	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\leftrightarrow \left(S\subseteq V\wedge \left(A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)\right)$$
32		3anass	$$⊢\left(S\subseteq V\wedge A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)\leftrightarrow \left(S\subseteq V\wedge \left(A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)\right)$$
33	31 32	bitr4i	$$⊢A\in \underset{\dot{}}{\perp }\left(S\right)\leftrightarrow \left(S\subseteq V\wedge A\in V\wedge \forall x\in SA\underset{\dot{}}{,}x=\underset{\dot{}}{0}\right)$$