Theorem vcidOLD

Description: Identity element for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) Obsolete theorem, use clmvs1 together with cvsclm instead. (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	vciOLD.1	|- G = ( 1st ` W )
	vciOLD.2	|- S = ( 2nd ` W )
	vciOLD.3	|- X = ran G
Assertion	vcidOLD	|- ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	|- G = ( 1st ` W )
2		vciOLD.2	|- S = ( 2nd ` W )
3		vciOLD.3	|- X = ran G
4	1 2 3	vciOLD	|- ( W e. CVecOLD -> ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) )
5		simpl	|- ( ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) -> ( 1 S x ) = x )
6	5	ralimi	|- ( A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) -> A. x e. X ( 1 S x ) = x )
7	6	3ad2ant3	|- ( ( G e. AbelOp /\ S : ( CC X. X ) --> X /\ A. x e. X ( ( 1 S x ) = x /\ A. y e. CC ( A. z e. X ( y S ( x G z ) ) = ( ( y S x ) G ( y S z ) ) /\ A. z e. CC ( ( ( y + z ) S x ) = ( ( y S x ) G ( z S x ) ) /\ ( ( y x. z ) S x ) = ( y S ( z S x ) ) ) ) ) ) -> A. x e. X ( 1 S x ) = x )
8	4 7	syl	|- ( W e. CVecOLD -> A. x e. X ( 1 S x ) = x )
9		oveq2	|- ( x = A -> ( 1 S x ) = ( 1 S A ) )
10		id	|- ( x = A -> x = A )
11	9 10	eqeq12d	|- ( x = A -> ( ( 1 S x ) = x <-> ( 1 S A ) = A ) )
12	11	rspccva	|- ( ( A. x e. X ( 1 S x ) = x /\ A e. X ) -> ( 1 S A ) = A )
13	8 12	sylan	|- ( ( W e. CVecOLD /\ A e. X ) -> ( 1 S A ) = A )