Metamath Proof Explorer

Theorem cvsi

Description: The properties of a subcomplex vector space, which is an Abelian group (i.e. the vectors, with the operation of vector addition) accompanied by a scalar multiplication operation on the field of complex numbers. (Contributed by NM, 3-Nov-2006) (Revised by AV, 21-Sep-2021)

Ref Expression
Hypotheses cvsi.x 
|- X = ( Base ` W )
cvsi.a 
|- .+ = ( +g ` W )
cvsi.s 
|- S = ( Base ` ( Scalar ` W ) )
cvsi.m 
|- .xb = ( .sf ` W )
cvsi.t 
|- .x. = ( .s ` W )
Assertion cvsi 
|- ( W e. CVec -> ( W e. Abel /\ ( S C_ CC /\ .xb : ( S X. X ) --> X ) /\ A. x e. X ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cvsi.x 
 |-  X = ( Base ` W )
2 cvsi.a 
 |-  .+ = ( +g ` W )
3 cvsi.s 
 |-  S = ( Base ` ( Scalar ` W ) )
4 cvsi.m 
 |-  .xb = ( .sf ` W )
5 cvsi.t 
 |-  .x. = ( .s ` W )
6 df-cvs 
 |-  CVec = ( CMod i^i LVec )
7 6 elin2 
 |-  ( W e. CVec <-> ( W e. CMod /\ W e. LVec ) )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 lmodabl 
 |-  ( W e. LMod -> W e. Abel )
10 8 9 syl 
 |-  ( W e. LVec -> W e. Abel )
11 10 adantl 
 |-  ( ( W e. CMod /\ W e. LVec ) -> W e. Abel )
12 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
13 12 3 clmsscn 
 |-  ( W e. CMod -> S C_ CC )
14 clmlmod 
 |-  ( W e. CMod -> W e. LMod )
15 1 12 3 4 lmodscaf 
 |-  ( W e. LMod -> .xb : ( S X. X ) --> X )
16 14 15 syl 
 |-  ( W e. CMod -> .xb : ( S X. X ) --> X )
17 13 16 jca 
 |-  ( W e. CMod -> ( S C_ CC /\ .xb : ( S X. X ) --> X ) )
18 17 adantr 
 |-  ( ( W e. CMod /\ W e. LVec ) -> ( S C_ CC /\ .xb : ( S X. X ) --> X ) )
19 1 5 clmvs1 
 |-  ( ( W e. CMod /\ x e. X ) -> ( 1 .x. x ) = x )
20 14 adantr 
 |-  ( ( W e. CMod /\ x e. X ) -> W e. LMod )
21 20 ad2antrr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. X ) -> W e. LMod )
22 simplr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. X ) -> y e. S )
23 simpllr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. X ) -> x e. X )
24 simpr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. X ) -> z e. X )
25 1 2 12 5 3 lmodvsdi 
 |-  ( ( W e. LMod /\ ( y e. S /\ x e. X /\ z e. X ) ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
26 21 22 23 24 25 syl13anc 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. X ) -> ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
27 26 ralrimiva 
 |-  ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) -> A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) )
28 12 clmadd 
 |-  ( W e. CMod -> + = ( +g ` ( Scalar ` W ) ) )
29 28 ad2antrr 
 |-  ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) -> + = ( +g ` ( Scalar ` W ) ) )
30 29 oveqdr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( y + z ) = ( y ( +g ` ( Scalar ` W ) ) z ) )
31 30 oveq1d 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( y + z ) .x. x ) = ( ( y ( +g ` ( Scalar ` W ) ) z ) .x. x ) )
32 20 ad2antrr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> W e. LMod )
33 simplr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> y e. S )
34 simpr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> z e. S )
35 simpllr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> x e. X )
36 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
37 1 2 12 5 3 36 lmodvsdir 
 |-  ( ( W e. LMod /\ ( y e. S /\ z e. S /\ x e. X ) ) -> ( ( y ( +g ` ( Scalar ` W ) ) z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) )
38 32 33 34 35 37 syl13anc 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( y ( +g ` ( Scalar ` W ) ) z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) )
39 31 38 eqtrd 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) )
40 12 clmmul 
 |-  ( W e. CMod -> x. = ( .r ` ( Scalar ` W ) ) )
41 40 ad2antrr 
 |-  ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) -> x. = ( .r ` ( Scalar ` W ) ) )
42 41 oveqdr 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( y x. z ) = ( y ( .r ` ( Scalar ` W ) ) z ) )
43 42 oveq1d 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( y x. z ) .x. x ) = ( ( y ( .r ` ( Scalar ` W ) ) z ) .x. x ) )
44 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
45 1 12 5 3 44 lmodvsass 
 |-  ( ( W e. LMod /\ ( y e. S /\ z e. S /\ x e. X ) ) -> ( ( y ( .r ` ( Scalar ` W ) ) z ) .x. x ) = ( y .x. ( z .x. x ) ) )
46 32 33 34 35 45 syl13anc 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( y ( .r ` ( Scalar ` W ) ) z ) .x. x ) = ( y .x. ( z .x. x ) ) )
47 43 46 eqtrd 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) )
48 39 47 jca 
 |-  ( ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) /\ z e. S ) -> ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) )
49 48 ralrimiva 
 |-  ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) -> A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) )
50 27 49 jca 
 |-  ( ( ( W e. CMod /\ x e. X ) /\ y e. S ) -> ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) )
51 50 ralrimiva 
 |-  ( ( W e. CMod /\ x e. X ) -> A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) )
52 19 51 jca 
 |-  ( ( W e. CMod /\ x e. X ) -> ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) )
53 52 ralrimiva 
 |-  ( W e. CMod -> A. x e. X ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) )
54 53 adantr 
 |-  ( ( W e. CMod /\ W e. LVec ) -> A. x e. X ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) )
55 11 18 54 3jca 
 |-  ( ( W e. CMod /\ W e. LVec ) -> ( W e. Abel /\ ( S C_ CC /\ .xb : ( S X. X ) --> X ) /\ A. x e. X ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) ) )
56 7 55 sylbi 
 |-  ( W e. CVec -> ( W e. Abel /\ ( S C_ CC /\ .xb : ( S X. X ) --> X ) /\ A. x e. X ( ( 1 .x. x ) = x /\ A. y e. S ( A. z e. X ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. z e. S ( ( ( y + z ) .x. x ) = ( ( y .x. x ) .+ ( z .x. x ) ) /\ ( ( y x. z ) .x. x ) = ( y .x. ( z .x. x ) ) ) ) ) ) )