Theorem obsipid

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

	Ref	Expression
Hypotheses	obsipid.h	|- ., = ( .i ` W )
	obsipid.f	|- F = ( Scalar ` W )
	obsipid.u	|- .1. = ( 1r ` F )
Assertion	obsipid	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( A ., A ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		obsipid.h	|- ., = ( .i ` W )
2		obsipid.f	|- F = ( Scalar ` W )
3		obsipid.u	|- .1. = ( 1r ` F )
4		eqid	|- ( Base ` W ) = ( Base ` W )
5		eqid	|- ( 0g ` F ) = ( 0g ` F )
6	4 1 2 3 5	obsip	|- ( ( B e. ( OBasis ` W ) /\ A e. B /\ A e. B ) -> ( A ., A ) = if ( A = A , .1. , ( 0g ` F ) ) )
7	6	3anidm23	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( A ., A ) = if ( A = A , .1. , ( 0g ` F ) ) )
8		eqid	|- A = A
9	8	iftruei	|- if ( A = A , .1. , ( 0g ` F ) ) = .1.
10	7 9	eqtrdi	|- ( ( B e. ( OBasis ` W ) /\ A e. B ) -> ( A ., A ) = .1. )