Theorem obsipid

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

	Ref	Expression
Hypotheses	obsipid.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	obsipid.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	obsipid.u	⊢ 1 = ( 1r ‘ 𝐹 )
Assertion	obsipid	⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 , 𝐴 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		obsipid.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
2		obsipid.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		obsipid.u	⊢ 1 = ( 1r ‘ 𝐹 )
4		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
6	4 1 2 3 5	obsip	⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 , 𝐴 ) = if ( 𝐴 = 𝐴 , 1 , ( 0g ‘ 𝐹 ) ) )
7	6	3anidm23	⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 , 𝐴 ) = if ( 𝐴 = 𝐴 , 1 , ( 0g ‘ 𝐹 ) ) )
8		eqid	⊢ 𝐴 = 𝐴
9	8	iftruei	⊢ if ( 𝐴 = 𝐴 , 1 , ( 0g ‘ 𝐹 ) ) = 1
10	7 9	eqtrdi	⊢ ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 , 𝐴 ) = 1 )