Metamath Proof Explorer

Theorem isvcOLD

Description: The predicate "is a complex vector space." (Contributed by NM, 31-May-2008) Obsolete version of iscvsp . (New usage is discouraged.) (Proof modification is discouraged.)

Ref

Expression

Hypothesis

isvcOLD.1

|- X = ran G

Assertion

|- ( <. G , S >. 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 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isvcOLD.1	\|- X = ran G
2		vcex	\|- ( <. G , S >. e. CVecOLD -> ( G e. _V /\ S e. _V ) )
3		elex	\|- ( G e. AbelOp -> G e. _V )
4	3	adantr	\|- ( ( G e. AbelOp /\ S : ( CC X. X ) --> X ) -> G e. _V )
5		cnex	\|- CC e. _V
6		ablogrpo	\|- ( G e. AbelOp -> G e. GrpOp )
7		rnexg	\|- ( G e. GrpOp -> ran G e. _V )
8	1 7	eqeltrid	\|- ( G e. GrpOp -> X e. _V )
9	6 8	syl	\|- ( G e. AbelOp -> X e. _V )
10		xpexg	\|- ( ( CC e. _V /\ X e. _V ) -> ( CC X. X ) e. _V )
11	5 9 10	sylancr	\|- ( G e. AbelOp -> ( CC X. X ) e. _V )
12		fex	\|- ( ( S : ( CC X. X ) --> X /\ ( CC X. X ) e. _V ) -> S e. _V )
13	11 12	sylan2	\|- ( ( S : ( CC X. X ) --> X /\ G e. AbelOp ) -> S e. _V )
14	13	ancoms	\|- ( ( G e. AbelOp /\ S : ( CC X. X ) --> X ) -> S e. _V )
15	4 14	jca	\|- ( ( G e. AbelOp /\ S : ( CC X. X ) --> X ) -> ( G e. _V /\ S e. _V ) )
16	15	3adant3	\|- ( ( 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 ) ) ) ) ) ) -> ( G e. _V /\ S e. _V ) )
17	1	isvclem	\|- ( ( G e. _V /\ S e. _V ) -> ( <. G , S >. 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 ) ) ) ) ) ) ) )
18	2 16 17	pm5.21nii	\|- ( <. G , S >. 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 ) ) ) ) ) ) )