Metamath Proof Explorer


Theorem obsss

Description: An orthonormal basis is a subset of the base set. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Hypothesis obsss.v 𝑉 = ( Base ‘ 𝑊 )
Assertion obsss ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝐵𝑉 )

Proof

Step Hyp Ref Expression
1 obsss.v 𝑉 = ( Base ‘ 𝑊 )
2 eqid ( ·𝑖𝑊 ) = ( ·𝑖𝑊 )
3 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4 eqid ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
5 eqid ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
6 eqid ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
7 eqid ( 0g𝑊 ) = ( 0g𝑊 )
8 1 2 3 4 5 6 7 isobs ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ↔ ( 𝑊 ∈ PreHil ∧ 𝐵𝑉 ∧ ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 ( ·𝑖𝑊 ) 𝑦 ) = if ( 𝑥 = 𝑦 , ( 1r ‘ ( Scalar ‘ 𝑊 ) ) , ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( ocv ‘ 𝑊 ) ‘ 𝐵 ) = { ( 0g𝑊 ) } ) ) )
9 8 simp2bi ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) → 𝐵𝑉 )