Theorem obsip

Description: The inner product of two elements of an orthonormal basis. (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$$
Assertion	obsip	$$⊢\left(B\in \mathrm{OBasis}\left(W\right)\wedge P\in B\wedge Q\in B\right)\to P\underset{\dot{}}{,}Q=if\left(P=Q,\underset{\dot{}}{1},\underset{\dot{}}{0}\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		eqid	$$⊢\mathrm{ocv}\left(W\right)=\mathrm{ocv}\left(W\right)$$
7		eqid	$$⊢0_W=0_W$$
8	1 2 3 4 5 6 7	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 \mathrm{ocv}\left(W\right)\left(B\right)=\left\{0_W\right\}\right)\right)$$
9	8	simp3bi	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\wedge \mathrm{ocv}\left(W\right)\left(B\right)=\left\{0_W\right\}\right)$$
10	9	simpld	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
11		oveq1	$$⊢x=P\to x\underset{\dot{}}{,}y=P\underset{\dot{}}{,}y$$
12		eqeq1	$$⊢x=P\to \left(x=y\leftrightarrow P=y\right)$$
13	12	ifbid	$$⊢x=P\to if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(P=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
14	11 13	eqeq12d	$$⊢x=P\to \left(x\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\leftrightarrow P\underset{\dot{}}{,}y=if\left(P=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
15		oveq2	$$⊢y=Q\to P\underset{\dot{}}{,}y=P\underset{\dot{}}{,}Q$$
16		eqeq2	$$⊢y=Q\to \left(P=y\leftrightarrow P=Q\right)$$
17	16	ifbid	$$⊢y=Q\to if\left(P=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(P=Q,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
18	15 17	eqeq12d	$$⊢y=Q\to \left(P\underset{\dot{}}{,}y=if\left(P=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\leftrightarrow P\underset{\dot{}}{,}Q=if\left(P=Q,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
19	14 18	rspc2v	$$⊢\left(P\in B\wedge Q\in B\right)\to \left(\forall x\in B\forall y\in Bx\underset{\dot{}}{,}y=if\left(x=y,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\to P\underset{\dot{}}{,}Q=if\left(P=Q,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
20	10 19	syl5com	$$⊢B\in \mathrm{OBasis}\left(W\right)\to \left(\left(P\in B\wedge Q\in B\right)\to P\underset{\dot{}}{,}Q=if\left(P=Q,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
21	20	3impib	$$⊢\left(B\in \mathrm{OBasis}\left(W\right)\wedge P\in B\wedge Q\in B\right)\to P\underset{\dot{}}{,}Q=if\left(P=Q,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$