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 = Scalar W
obsipid.u 1 ˙ = 1 F
Assertion obsipid B OBasis W A B A , ˙ A = 1 ˙

Proof

Step Hyp Ref Expression
1 obsipid.h , ˙ = 𝑖 W
2 obsipid.f F = Scalar W
3 obsipid.u 1 ˙ = 1 F
4 eqid Base W = Base W
5 eqid 0 F = 0 F
6 4 1 2 3 5 obsip B OBasis W A B A B A , ˙ A = if A = A 1 ˙ 0 F
7 6 3anidm23 B OBasis W A B A , ˙ A = if A = A 1 ˙ 0 F
8 eqid A = A
9 8 iftruei if A = A 1 ˙ 0 F = 1 ˙
10 7 9 eqtrdi B OBasis W A B A , ˙ A = 1 ˙