This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )