Metamath Proof Explorer

Theorem cnlmod

Description: The set of complex numbers is a left module over itself. The vector operation is + , and the scalar product is x. . (Contributed by AV, 20-Sep-2021)

Ref Expression
Hypothesis cnlmod.w 
|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
Assertion cnlmod 
|- W e. LMod

Proof

Step Hyp Ref Expression
1 cnlmod.w 
 |-  W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
2 0cn 
 |-  0 e. CC
3 1 cnlmodlem1 
 |-  ( Base ` W ) = CC
4 3 eqcomi 
 |-  CC = ( Base ` W )
5 4 a1i 
 |-  ( 0 e. CC -> CC = ( Base ` W ) )
6 1 cnlmodlem2 
 |-  ( +g ` W ) = +
7 6 eqcomi 
 |-  + = ( +g ` W )
8 7 a1i 
 |-  ( 0 e. CC -> + = ( +g ` W ) )
9 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
10 9 3adant1 
 |-  ( ( 0 e. CC /\ x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
11 addass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
12 11 adantl 
 |-  ( ( 0 e. CC /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
13 id 
 |-  ( 0 e. CC -> 0 e. CC )
14 addlid 
 |-  ( x e. CC -> ( 0 + x ) = x )
15 14 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 + x ) = x )
16 negcl 
 |-  ( x e. CC -> -u x e. CC )
17 16 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> -u x e. CC )
18 id 
 |-  ( x e. CC -> x e. CC )
19 16 18 addcomd 
 |-  ( x e. CC -> ( -u x + x ) = ( x + -u x ) )
20 19 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( -u x + x ) = ( x + -u x ) )
21 negid 
 |-  ( x e. CC -> ( x + -u x ) = 0 )
22 21 adantl 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( x + -u x ) = 0 )
23 20 22 eqtrd 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( -u x + x ) = 0 )
24 5 8 10 12 13 15 17 23 isgrpd 
 |-  ( 0 e. CC -> W e. Grp )
25 4 a1i 
 |-  ( W e. Grp -> CC = ( Base ` W ) )
26 7 a1i 
 |-  ( W e. Grp -> + = ( +g ` W ) )
27 1 cnlmodlem3 
 |-  ( Scalar ` W ) = CCfld
28 27 eqcomi 
 |-  CCfld = ( Scalar ` W )
29 28 a1i 
 |-  ( W e. Grp -> CCfld = ( Scalar ` W ) )
30 1 cnlmod4 
 |-  ( .s ` W ) = x.
31 30 eqcomi 
 |-  x. = ( .s ` W )
32 31 a1i 
 |-  ( W e. Grp -> x. = ( .s ` W ) )
33 cnfldbas 
 |-  CC = ( Base ` CCfld )
34 33 a1i 
 |-  ( W e. Grp -> CC = ( Base ` CCfld ) )
35 cnfldadd 
 |-  + = ( +g ` CCfld )
36 35 a1i 
 |-  ( W e. Grp -> + = ( +g ` CCfld ) )
37 cnfldmul 
 |-  x. = ( .r ` CCfld )
38 37 a1i 
 |-  ( W e. Grp -> x. = ( .r ` CCfld ) )
39 cnfld1 
 |-  1 = ( 1r ` CCfld )
40 39 a1i 
 |-  ( W e. Grp -> 1 = ( 1r ` CCfld ) )
41 cnring 
 |-  CCfld e. Ring
42 41 a1i 
 |-  ( W e. Grp -> CCfld e. Ring )
43 id 
 |-  ( W e. Grp -> W e. Grp )
44 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
45 44 3adant1 
 |-  ( ( W e. Grp /\ x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
46 adddi 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
47 46 adantl 
 |-  ( ( W e. Grp /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
48 adddir 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
49 48 adantl 
 |-  ( ( W e. Grp /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x + y ) x. z ) = ( ( x x. z ) + ( y x. z ) ) )
50 mulass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
51 50 adantl 
 |-  ( ( W e. Grp /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x x. y ) x. z ) = ( x x. ( y x. z ) ) )
52 mullid 
 |-  ( x e. CC -> ( 1 x. x ) = x )
53 52 adantl 
 |-  ( ( W e. Grp /\ x e. CC ) -> ( 1 x. x ) = x )
54 25 26 29 32 34 36 38 40 42 43 45 47 49 51 53 islmodd 
 |-  ( W e. Grp -> W e. LMod )
55 2 24 54 mp2b 
 |-  W e. LMod