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