Theorem obsipid

Description: A basis element has length one. (Contributed by Mario Carneiro, 23-Oct-2015)

	Ref	Expression
Hypotheses	obsipid.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	obsipid.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	obsipid.u	$$⊢\underset{\dot{}}{1}=1_F$$
Assertion	obsipid	$$⊢\left(B\in \mathrm{OBasis}\left(W\right)\wedge A\in B\right)\to A\underset{\dot{}}{,}A=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		obsipid.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		obsipid.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
3		obsipid.u	$$⊢\underset{\dot{}}{1}=1_F$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5		eqid	$$⊢0_F=0_F$$
6	4 1 2 3 5	obsip	$$⊢\left(B\in \mathrm{OBasis}\left(W\right)\wedge A\in B\wedge A\in B\right)\to A\underset{\dot{}}{,}A=if\left(A=A,\underset{\dot{}}{1},0_F\right)$$
7	6	3anidm23	$$⊢\left(B\in \mathrm{OBasis}\left(W\right)\wedge A\in B\right)\to A\underset{\dot{}}{,}A=if\left(A=A,\underset{\dot{}}{1},0_F\right)$$
8		eqid	$$⊢A=A$$
9	8	iftruei	$$⊢if\left(A=A,\underset{\dot{}}{1},0_F\right)=\underset{\dot{}}{1}$$
10	7 9	eqtrdi	$$⊢\left(B\in \mathrm{OBasis}\left(W\right)\wedge A\in B\right)\to A\underset{\dot{}}{,}A=\underset{\dot{}}{1}$$