Metamath Proof Explorer


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 )