Metamath Proof Explorer


Theorem obsipid

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

Ref Expression
Hypotheses obsipid.h ,˙=𝑖W
obsipid.f F=ScalarW
obsipid.u 1˙=1F
Assertion obsipid BOBasisWABA,˙A=1˙

Proof

Step Hyp Ref Expression
1 obsipid.h ,˙=𝑖W
2 obsipid.f F=ScalarW
3 obsipid.u 1˙=1F
4 eqid BaseW=BaseW
5 eqid 0F=0F
6 4 1 2 3 5 obsip BOBasisWABABA,˙A=ifA=A1˙0F
7 6 3anidm23 BOBasisWABA,˙A=ifA=A1˙0F
8 eqid A=A
9 8 iftruei ifA=A1˙0F=1˙
10 7 9 eqtrdi BOBasisWABA,˙A=1˙