Metamath Proof Explorer

Theorem isclmi0

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

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

Proof

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