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

Metamath Proof Explorer

Theorem iscvsi

Description: Properties that determine a subcomplex vector space. (Contributed by NM, 5-Nov-2006) (Revised by AV, 4-Oct-2021)

Ref Expression
Hypotheses iscvsp.t 
|- .x. = ( .s ` W )
iscvsp.a 
|- .+ = ( +g ` W )
iscvsp.v 
|- V = ( Base ` W )
iscvsp.s 
|- S = ( Scalar ` W )
iscvsp.k 
|- K = ( Base ` S )
iscvsi.1 
|- W e. Grp
iscvsi.2 
|- S = ( CCfld |`s K )
iscvsi.3 
|- S e. DivRing
iscvsi.4 
|- K e. ( SubRing ` CCfld )
iscvsi.5 
|- ( x e. V -> ( 1 .x. x ) = x )
iscvsi.6 
|- ( ( y e. K /\ x e. V ) -> ( y .x. x ) e. V )
iscvsi.7 
|- ( ( y e. K /\ x e. V /\ z e. V ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
iscvsi.8 
|- ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) )
iscvsi.9 
|- ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) )
Assertion iscvsi 
|- W e. CVec

Proof

Step Hyp Ref Expression
1 iscvsp.t 
 |-  .x. = ( .s ` W )
2 iscvsp.a 
 |-  .+ = ( +g ` W )
3 iscvsp.v 
 |-  V = ( Base ` W )
4 iscvsp.s 
 |-  S = ( Scalar ` W )
5 iscvsp.k 
 |-  K = ( Base ` S )
6 iscvsi.1 
 |-  W e. Grp
7 iscvsi.2 
 |-  S = ( CCfld |`s K )
8 iscvsi.3 
 |-  S e. DivRing
9 iscvsi.4 
 |-  K e. ( SubRing ` CCfld )
10 iscvsi.5 
 |-  ( x e. V -> ( 1 .x. x ) = x )
11 iscvsi.6 
 |-  ( ( y e. K /\ x e. V ) -> ( y .x. x ) e. V )
12 iscvsi.7 
 |-  ( ( y e. K /\ x e. V /\ z e. V ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
13 iscvsi.8 
 |-  ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) )
14 iscvsi.9 
 |-  ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) )
15 8 7 pm3.2i 
 |-  ( S e. DivRing /\ S = ( CCfld |`s K ) )
16 6 15 9 3pm3.2i 
 |-  ( W e. Grp /\ ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ K e. ( SubRing ` CCfld ) )
17 11 ancoms 
 |-  ( ( x e. V /\ y e. K ) -> ( y .x. x ) e. V )
18 12 3com12 
 |-  ( ( x e. V /\ y e. K /\ z e. V ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
19 18 3expa 
 |-  ( ( ( x e. V /\ y e. K ) /\ z e. V ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
20 19 ralrimiva 
 |-  ( ( x e. V /\ y e. K ) -> A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
21 13 14 jca 
 |-  ( ( y e. K /\ z e. K /\ x e. V ) -> ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) )
22 21 3comr 
 |-  ( ( x e. V /\ y e. K /\ z e. K ) -> ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) )
23 22 3expa 
 |-  ( ( ( x e. V /\ y e. K ) /\ z e. K ) -> ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) )
24 23 ralrimiva 
 |-  ( ( x e. V /\ y e. K ) -> A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) )
25 17 20 24 3jca 
 |-  ( ( x e. V /\ y e. K ) -> ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) )
26 25 ralrimiva 
 |-  ( x e. V -> A. y e. K ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) )
27 10 26 jca 
 |-  ( x e. V -> ( ( 1 .x. x ) = x /\ A. y e. K ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) ) )
28 27 rgen 
 |-  A. x e. V ( ( 1 .x. x ) = x /\ A. y e. K ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) )
29 1 2 3 4 5 iscvsp 
 |-  ( W e. CVec <-> ( ( W e. Grp /\ ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ K e. ( SubRing ` CCfld ) ) /\ A. x e. V ( ( 1 .x. x ) = x /\ A. y e. K ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) ) ) ) )
30 16 28 29 mpbir2an 
 |-  W e. CVec