Metamath Proof Explorer

Theorem iscvsp

Description: The predicate "is a subcomplex vector space". (Contributed by NM, 31-May-2008) (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 )
Assertion 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 ) ) ) ) ) ) )

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 iscvs 
 |-  ( W e. CVec <-> ( W e. CMod /\ ( Scalar ` W ) e. DivRing ) )
7 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 ) ) ) ) ) ) )
8 7 anbi2ci 
 |-  ( ( W e. CMod /\ ( Scalar ` W ) e. DivRing ) <-> ( ( Scalar ` W ) e. DivRing /\ ( ( 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 ) ) ) ) ) ) ) )
9 anass 
 |-  ( ( ( ( Scalar ` W ) e. DivRing /\ ( 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 ) ) ) ) ) ) <-> ( ( Scalar ` W ) e. DivRing /\ ( ( 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 ) ) ) ) ) ) ) )
10 3anan12 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( S = ( CCfld |`s K ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) )
11 10 anbi2i 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( Scalar ` W ) e. DivRing /\ ( S = ( CCfld |`s K ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) ) )
12 anass 
 |-  ( ( ( ( Scalar ` W ) e. DivRing /\ S = ( CCfld |`s K ) ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( Scalar ` W ) e. DivRing /\ ( S = ( CCfld |`s K ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) ) )
13 4 eqcomi 
 |-  ( Scalar ` W ) = S
14 13 eleq1i 
 |-  ( ( Scalar ` W ) e. DivRing <-> S e. DivRing )
15 14 anbi1i 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ S = ( CCfld |`s K ) ) <-> ( S e. DivRing /\ S = ( CCfld |`s K ) ) )
16 15 anbi1i 
 |-  ( ( ( ( Scalar ` W ) e. DivRing /\ S = ( CCfld |`s K ) ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) )
17 11 12 16 3bitr2i 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) )
18 3anan12 
 |-  ( ( W e. Grp /\ ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ K e. ( SubRing ` CCfld ) ) <-> ( ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ ( W e. Grp /\ K e. ( SubRing ` CCfld ) ) ) )
19 17 18 bitr4i 
 |-  ( ( ( Scalar ` W ) e. DivRing /\ ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( W e. Grp /\ ( S e. DivRing /\ S = ( CCfld |`s K ) ) /\ K e. ( SubRing ` CCfld ) ) )
20 19 anbi1i 
 |-  ( ( ( ( Scalar ` W ) e. DivRing /\ ( 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 ) ) ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
21 8 9 20 3bitr2i 
 |-  ( ( W e. CMod /\ ( Scalar ` W ) e. DivRing ) <-> ( ( 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 ) ) ) ) ) ) )
22 6 21 bitri 
 |-  ( 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 ) ) ) ) ) ) )