Theorem isobs

Description: The predicate "is an orthonormal basis" (over a pre-Hilbert space). (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	isobs.v	$$⊢V={\mathrm{Base}}_W$$
	isobs.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	isobs.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	isobs.u	$$⊢\underset{\dot{}}{1}=1_F$$
	isobs.z	$$⊢\underset{\dot{}}{0}=0_F$$
	isobs.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
	isobs.y	$$⊢Y=0_W$$
Assertion	isobs	$$⊢B\in \mathrm{OBasis}\left(W\right)\leftrightarrow \left(W\in \mathrm{PreHil}\wedge B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isobs.v	$$⊢V={\mathrm{Base}}_W$$
2		isobs.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		isobs.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		isobs.u	$$⊢\underset{\dot{}}{1}=1_F$$
5		isobs.z	$$⊢\underset{\dot{}}{0}=0_F$$
6		isobs.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocv}\left(W\right)$$
7		isobs.y	$$⊢Y=0_W$$
8		df-obs	$$⊢\mathrm{OBasis}=\left(h\in \mathrm{PreHil}⟼\left\{b\in 𝒫{\mathrm{Base}}_h|\left(\forall x\in b\forall y\in bx{\cdot }_{𝑖}\left(h\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(h\right)},0_{\mathrm{Scalar}\left(h\right)}\right)\wedge \mathrm{ocv}\left(h\right)\left(b\right)=\left\{0_h\right\}\right)\right\}\right)$$
9	8	mptrcl	$$⊢B\in \mathrm{OBasis}\left(W\right)\to W\in \mathrm{PreHil}$$
10		fveq2	$$⊢h=W\to {\mathrm{Base}}_h={\mathrm{Base}}_W$$
11	10 1	eqtr4di	$$⊢h=W\to {\mathrm{Base}}_h=V$$
12	11	pweqd	$$⊢h=W\to 𝒫{\mathrm{Base}}_h=𝒫V$$
13		fveq2	$$⊢h=W\to {\cdot }_{𝑖}\left(h\right)={\cdot }_{𝑖}\left(W\right)$$
14	13 2	eqtr4di	$$⊢h=W\to {\cdot }_{𝑖}\left(h\right)=\underset{\dot{}}{,}$$
15	14	oveqd	$$⊢h=W\to x{\cdot }_{𝑖}\left(h\right)y=x\underset{\dot{}}{,}y$$
16		fveq2	$$⊢h=W\to \mathrm{Scalar}\left(h\right)=\mathrm{Scalar}\left(W\right)$$
17	16 3	eqtr4di	$$⊢h=W\to \mathrm{Scalar}\left(h\right)=F$$
18	17	fveq2d	$$⊢h=W\to 1_{\mathrm{Scalar}\left(h\right)}=1_F$$
19	18 4	eqtr4di	$$⊢h=W\to 1_{\mathrm{Scalar}\left(h\right)}=\underset{\dot{}}{1}$$
20	17	fveq2d	$$⊢h=W\to 0_{\mathrm{Scalar}\left(h\right)}=0_F$$
21	20 5	eqtr4di	$$⊢h=W\to 0_{\mathrm{Scalar}\left(h\right)}=\underset{\dot{}}{0}$$
22	19 21	ifeq12d	$$⊢h=W\to if\left(x=y,1_{\mathrm{Scalar}\left(h\right)},0_{\mathrm{Scalar}\left(h\right)}\right)=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
23	15 22	eqeq12d	$$⊢h=W\to \left(x{\cdot }_{𝑖}\left(h\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(h\right)},0_{\mathrm{Scalar}\left(h\right)}\right)\leftrightarrow x\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
24	23	2ralbidv	$$⊢h=W\to \left(\forall x\in b\forall y\in bx{\cdot }_{𝑖}\left(h\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(h\right)},0_{\mathrm{Scalar}\left(h\right)}\right)\leftrightarrow \forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
25		fveq2	$$⊢h=W\to \mathrm{ocv}\left(h\right)=\mathrm{ocv}\left(W\right)$$
26	25 6	eqtr4di	$$⊢h=W\to \mathrm{ocv}\left(h\right)=\underset{\dot{}}{\perp }$$
27	26	fveq1d	$$⊢h=W\to \mathrm{ocv}\left(h\right)\left(b\right)=\underset{\dot{}}{\perp }\left(b\right)$$
28		fveq2	$$⊢h=W\to 0_h=0_W$$
29	28 7	eqtr4di	$$⊢h=W\to 0_h=Y$$
30	29	sneqd	$$⊢h=W\to \left\{0_h\right\}=\left\{Y\right\}$$
31	27 30	eqeq12d	$$⊢h=W\to \left(\mathrm{ocv}\left(h\right)\left(b\right)=\left\{0_h\right\}\leftrightarrow \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)$$
32	24 31	anbi12d	$$⊢h=W\to \left(\left(\forall x\in b\forall y\in bx{\cdot }_{𝑖}\left(h\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(h\right)},0_{\mathrm{Scalar}\left(h\right)}\right)\wedge \mathrm{ocv}\left(h\right)\left(b\right)=\left\{0_h\right\}\right)\leftrightarrow \left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right)$$
33	12 32	rabeqbidv	$$⊢h=W\to \left\{b\in 𝒫{\mathrm{Base}}_h|\left(\forall x\in b\forall y\in bx{\cdot }_{𝑖}\left(h\right)y=if\left(x=y,1_{\mathrm{Scalar}\left(h\right)},0_{\mathrm{Scalar}\left(h\right)}\right)\wedge \mathrm{ocv}\left(h\right)\left(b\right)=\left\{0_h\right\}\right)\right\}=\left\{b\in 𝒫V|\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right\}$$
34	1	fvexi	$$⊢V\in \mathrm{V}$$
35	34	pwex	$$⊢𝒫V\in \mathrm{V}$$
36	35	rabex	$$⊢\left\{b\in 𝒫V|\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right\}\in \mathrm{V}$$
37	33 8 36	fvmpt	$$⊢W\in \mathrm{PreHil}\to \mathrm{OBasis}\left(W\right)=\left\{b\in 𝒫V|\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right\}$$
38	37	eleq2d	$$⊢W\in \mathrm{PreHil}\to \left(B\in \mathrm{OBasis}\left(W\right)\leftrightarrow B\in \left\{b\in 𝒫V|\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right\}\right)$$
39		raleq	$$⊢b=B\to \left(\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\leftrightarrow \forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
40	39	raleqbi1dv	$$⊢b=B\to \left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\leftrightarrow \forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
41		fveqeq2	$$⊢b=B\to \left(\underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\leftrightarrow \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)$$
42	40 41	anbi12d	$$⊢b=B\to \left(\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\leftrightarrow \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)$$
43	42	elrab	$$⊢B\in \left\{b\in 𝒫V|\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right\}\leftrightarrow \left(B\in 𝒫V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)$$
44	34	elpw2	$$⊢B\in 𝒫V\leftrightarrow B\subseteq V$$
45	44	anbi1i	$$⊢\left(B\in 𝒫V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)\leftrightarrow \left(B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)$$
46	43 45	bitri	$$⊢B\in \left\{b\in 𝒫V|\left(\forall x\in b\forall y\in bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(b\right)=\left\{Y\right\}\right)\right\}\leftrightarrow \left(B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)$$
47	38 46	bitrdi	$$⊢W\in \mathrm{PreHil}\to \left(B\in \mathrm{OBasis}\left(W\right)\leftrightarrow \left(B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)\right)$$
48	9 47	biadanii	$$⊢B\in \mathrm{OBasis}\left(W\right)\leftrightarrow \left(W\in \mathrm{PreHil}\wedge \left(B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)\right)$$
49		3anass	$$⊢\left(W\in \mathrm{PreHil}\wedge B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)\leftrightarrow \left(W\in \mathrm{PreHil}\wedge \left(B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)\right)$$
50	48 49	bitr4i	$$⊢B\in \mathrm{OBasis}\left(W\right)\leftrightarrow \left(W\in \mathrm{PreHil}\wedge B\subseteq V\wedge \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \underset{\dot{}}{\perp }\left(B\right)=\left\{Y\right\}\right)\right)$$