Metamath Proof Explorer

Theorem isclmp

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

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 4 5 isclm 
 |-  ( W e. CMod <-> ( W e. LMod /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) )
7 eqid 
 |-  ( +g ` S ) = ( +g ` S )
8 eqid 
 |-  ( .r ` S ) = ( .r ` S )
9 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
10 3 2 1 4 5 7 8 9 islmod 
 |-  ( W e. LMod <-> ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) )
11 10 3anbi1i 
 |-  ( ( W e. LMod /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) )
12 3anass 
 |-  ( ( ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
13 df-3an 
 |-  ( ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) <-> ( ( W e. Grp /\ S e. Ring ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) )
14 13 anbi1i 
 |-  ( ( ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( ( W e. Grp /\ S e. Ring ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
15 12 14 bitri 
 |-  ( ( ( W e. Grp /\ S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( ( ( W e. Grp /\ S e. Ring ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
16 an32 
 |-  ( ( ( ( W e. Grp /\ S e. Ring ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) )
17 11 15 16 3bitri 
 |-  ( ( W e. LMod /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) )
18 an32 
 |-  ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( W e. Grp /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) /\ S e. Ring ) )
19 3anass 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) <-> ( W e. Grp /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) )
20 19 bicomi 
 |-  ( ( W e. Grp /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) )
21 20 anbi1i 
 |-  ( ( ( W e. Grp /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) /\ S e. Ring ) <-> ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ S e. Ring ) )
22 18 21 bitri 
 |-  ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) <-> ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ S e. Ring ) )
23 22 anbi1i 
 |-  ( ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) <-> ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ S e. Ring ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) )
24 anass 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ S e. Ring ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) <-> ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) ) )
25 df-3an 
 |-  ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) <-> ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) )
26 ancom 
 |-  ( ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) <-> ( ( ( 1r ` S ) .x. x ) = x /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) )
27 25 26 anbi12i 
 |-  ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( 1r ` S ) .x. x ) = x /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
28 an4 
 |-  ( ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( 1r ` S ) .x. x ) = x /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( 1r ` S ) .x. x ) = x ) /\ ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
29 an32 
 |-  ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( 1r ` S ) .x. x ) = x ) <-> ( ( ( y .x. x ) e. V /\ ( ( 1r ` S ) .x. x ) = x ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
30 ancom 
 |-  ( ( ( y .x. x ) e. V /\ ( ( 1r ` S ) .x. x ) = x ) <-> ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) )
31 30 anbi1i 
 |-  ( ( ( ( y .x. x ) e. V /\ ( ( 1r ` S ) .x. x ) = x ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
32 29 31 bitri 
 |-  ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( 1r ` S ) .x. x ) = x ) <-> ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
33 32 anbi1i 
 |-  ( ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( 1r ` S ) .x. x ) = x ) /\ ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
34 27 28 33 3bitri 
 |-  ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> ( ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
35 fveq2 
 |-  ( S = ( CCfld |`s K ) -> ( 1r ` S ) = ( 1r ` ( CCfld |`s K ) ) )
36 eqid 
 |-  ( CCfld |`s K ) = ( CCfld |`s K )
37 eqid 
 |-  ( 1r ` CCfld ) = ( 1r ` CCfld )
38 36 37 subrg1 
 |-  ( K e. ( SubRing ` CCfld ) -> ( 1r ` CCfld ) = ( 1r ` ( CCfld |`s K ) ) )
39 38 eqcomd 
 |-  ( K e. ( SubRing ` CCfld ) -> ( 1r ` ( CCfld |`s K ) ) = ( 1r ` CCfld ) )
40 35 39 sylan9eq 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( 1r ` S ) = ( 1r ` CCfld ) )
41 cnfld1 
 |-  1 = ( 1r ` CCfld )
42 40 41 eqtr4di 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( 1r ` S ) = 1 )
43 42 oveq1d 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( ( 1r ` S ) .x. x ) = ( 1 .x. x ) )
44 43 eqeq1d 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( ( ( 1r ` S ) .x. x ) = x <-> ( 1 .x. x ) = x ) )
45 44 3adant1 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( ( ( 1r ` S ) .x. x ) = x <-> ( 1 .x. x ) = x ) )
46 45 ad2antrr 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( 1r ` S ) .x. x ) = x <-> ( 1 .x. x ) = x ) )
47 46 anbi1d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) <-> ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) )
48 47 anbi1d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
49 eqid 
 |-  ( +g ` CCfld ) = ( +g ` CCfld )
50 36 49 ressplusg 
 |-  ( K e. ( SubRing ` CCfld ) -> ( +g ` CCfld ) = ( +g ` ( CCfld |`s K ) ) )
51 50 adantl 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( +g ` CCfld ) = ( +g ` ( CCfld |`s K ) ) )
52 cnfldadd 
 |-  + = ( +g ` CCfld )
53 52 a1i 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> + = ( +g ` CCfld ) )
54 fveq2 
 |-  ( S = ( CCfld |`s K ) -> ( +g ` S ) = ( +g ` ( CCfld |`s K ) ) )
55 54 adantr 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( +g ` S ) = ( +g ` ( CCfld |`s K ) ) )
56 51 53 55 3eqtr4rd 
 |-  ( ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( +g ` S ) = + )
57 56 3adant1 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( +g ` S ) = + )
58 57 oveqd 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( r ( +g ` S ) y ) = ( r + y ) )
59 58 ad2antrr 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( r ( +g ` S ) y ) = ( r + y ) )
60 59 oveq1d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( r ( +g ` S ) y ) .x. x ) = ( ( r + y ) .x. x ) )
61 60 eqeq1d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) <-> ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) )
62 eqid 
 |-  ( .r ` CCfld ) = ( .r ` CCfld )
63 36 62 ressmulr 
 |-  ( K e. ( SubRing ` CCfld ) -> ( .r ` CCfld ) = ( .r ` ( CCfld |`s K ) ) )
64 63 3ad2ant3 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( .r ` CCfld ) = ( .r ` ( CCfld |`s K ) ) )
65 cnfldmul 
 |-  x. = ( .r ` CCfld )
66 65 a1i 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> x. = ( .r ` CCfld ) )
67 fveq2 
 |-  ( S = ( CCfld |`s K ) -> ( .r ` S ) = ( .r ` ( CCfld |`s K ) ) )
68 67 3ad2ant2 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( .r ` S ) = ( .r ` ( CCfld |`s K ) ) )
69 64 66 68 3eqtr4rd 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( .r ` S ) = x. )
70 69 oveqd 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( r ( .r ` S ) y ) = ( r x. y ) )
71 70 ad2antrr 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( r ( .r ` S ) y ) = ( r x. y ) )
72 71 oveq1d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( r ( .r ` S ) y ) .x. x ) = ( ( r x. y ) .x. x ) )
73 72 eqeq1d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) <-> ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) )
74 61 73 anbi12d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) <-> ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
75 48 74 anbi12d 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
76 34 75 syl5bb 
 |-  ( ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
77 76 2ralbidva 
 |-  ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( r e. K /\ y e. K ) ) -> ( A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> A. z e. V A. x e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
78 77 2ralbidva 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
79 ralrot3 
 |-  ( A. y e. K A. z e. V A. x e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. x e. V A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
80 79 ralbii 
 |-  ( A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. r e. K A. x e. V A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
81 ralcom 
 |-  ( A. r e. K A. x e. V A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. x e. V A. r e. K A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
82 80 81 bitri 
 |-  ( A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. x e. V A. r e. K A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
83 ralcom 
 |-  ( A. r e. K A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. y e. K A. r e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
84 83 ralbii 
 |-  ( A. x e. V A. r e. K A. y e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. x e. V A. y e. K A. r e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
85 ralcom 
 |-  ( A. r e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
86 85 2ralbii 
 |-  ( A. x e. V A. y e. K A. r e. K A. z e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. x e. V A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
87 82 84 86 3bitri 
 |-  ( A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. x e. V A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
88 78 87 bitrdi 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> A. x e. V A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
89 36 subrgring 
 |-  ( K e. ( SubRing ` CCfld ) -> ( CCfld |`s K ) e. Ring )
90 89 3ad2ant3 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( CCfld |`s K ) e. Ring )
91 eleq1 
 |-  ( S = ( CCfld |`s K ) -> ( S e. Ring <-> ( CCfld |`s K ) e. Ring ) )
92 91 3ad2ant2 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( S e. Ring <-> ( CCfld |`s K ) e. Ring ) )
93 90 92 mpbird 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> S e. Ring )
94 93 biantrurd 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) <-> ( S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) ) )
95 3 grpbn0 
 |-  ( W e. Grp -> V =/= (/) )
96 95 3ad2ant1 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> V =/= (/) )
97 37 subrg1cl 
 |-  ( K e. ( SubRing ` CCfld ) -> ( 1r ` CCfld ) e. K )
98 97 ne0d 
 |-  ( K e. ( SubRing ` CCfld ) -> K =/= (/) )
99 98 3ad2ant3 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> K =/= (/) )
100 ancom 
 |-  ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) )
101 100 anbi1i 
 |-  ( ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
102 101 a1i 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
103 102 ralbidv 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. r e. K ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
104 r19.28zv 
 |-  ( K =/= (/) -> ( A. r e. K ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
105 104 adantl 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. r e. K ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
106 103 105 bitrd 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
107 anass 
 |-  ( ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
108 anass 
 |-  ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) )
109 108 anbi2i 
 |-  ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) <-> ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) ) )
110 ancom 
 |-  ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
111 107 109 110 3bitri 
 |-  ( ( ( ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
112 106 111 bitrdi 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
113 112 ralbidv 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. z e. V ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
114 r19.28zv 
 |-  ( V =/= (/) -> ( A. z e. V ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
115 114 adantr 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. z e. V ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
116 113 115 bitrd 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
117 anass 
 |-  ( ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( 1 .x. x ) = x /\ ( ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) )
118 oveq1 
 |-  ( z = r -> ( z + y ) = ( r + y ) )
119 118 oveq1d 
 |-  ( z = r -> ( ( z + y ) .x. x ) = ( ( r + y ) .x. x ) )
120 oveq1 
 |-  ( z = r -> ( z .x. x ) = ( r .x. x ) )
121 120 oveq1d 
 |-  ( z = r -> ( ( z .x. x ) .+ ( y .x. x ) ) = ( ( r .x. x ) .+ ( y .x. x ) ) )
122 119 121 eqeq12d 
 |-  ( z = r -> ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) <-> ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) )
123 oveq1 
 |-  ( z = r -> ( z x. y ) = ( r x. y ) )
124 123 oveq1d 
 |-  ( z = r -> ( ( z x. y ) .x. x ) = ( ( r x. y ) .x. x ) )
125 oveq1 
 |-  ( z = r -> ( z .x. ( y .x. x ) ) = ( r .x. ( y .x. x ) ) )
126 124 125 eqeq12d 
 |-  ( z = r -> ( ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) <-> ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) )
127 122 126 anbi12d 
 |-  ( z = r -> ( ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) <-> ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
128 127 cbvralvw 
 |-  ( A. z e. K ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) /\ ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) ) <-> A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) )
129 128 3anbi3i 
 |-  ( ( ( 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 ) ) ) ) <-> ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) )
130 3anan32 
 |-  ( ( ( y .x. x ) e. V /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
131 129 130 bitri 
 |-  ( ( ( 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 ) ) ) ) <-> ( ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) )
132 131 bicomi 
 |-  ( ( ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( 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 ) ) ) ) )
133 132 anbi2i 
 |-  ( ( ( 1 .x. x ) = x /\ ( ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) ) <-> ( ( 1 .x. x ) = x /\ ( ( 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 ) ) ) ) ) )
134 117 133 bitri 
 |-  ( ( ( ( 1 .x. x ) = x /\ ( ( y .x. x ) e. V /\ A. r e. K ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) ) /\ A. z e. V ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) <-> ( ( 1 .x. x ) = x /\ ( ( 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 ) ) ) ) ) )
135 116 134 bitrdi 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( 1 .x. x ) = x /\ ( ( 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 ) ) ) ) ) ) )
136 135 ralbidv 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> A. y e. K ( ( 1 .x. x ) = x /\ ( ( 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 ) ) ) ) ) ) )
137 r19.28zv 
 |-  ( K =/= (/) -> ( A. y e. K ( ( 1 .x. x ) = x /\ ( ( 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 ) ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
138 137 adantl 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. y e. K ( ( 1 .x. x ) = x /\ ( ( 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 ) ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
139 136 138 bitrd 
 |-  ( ( V =/= (/) /\ K =/= (/) ) -> ( A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
140 96 99 139 syl2anc 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
141 140 ralbidv 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( A. x e. V A. y e. K A. z e. V A. r e. K ( ( ( ( 1 .x. x ) = x /\ ( y .x. x ) e. V ) /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) ) /\ ( ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) /\ ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) ) <-> 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 ) ) ) ) ) ) )
142 88 94 141 3bitr3d 
 |-  ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) -> ( ( S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) <-> 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 ) ) ) ) ) ) )
143 142 pm5.32i 
 |-  ( ( ( W e. Grp /\ S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) /\ ( S e. Ring /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
144 23 24 143 3bitri 
 |-  ( ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = ( CCfld |`s K ) /\ K e. ( SubRing ` CCfld ) ) ) /\ A. r e. K A. y e. K A. z e. V A. x e. V ( ( ( y .x. x ) e. V /\ ( y .x. ( x .+ z ) ) = ( ( y .x. x ) .+ ( y .x. z ) ) /\ ( ( r ( +g ` S ) y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) /\ ( ( ( r ( .r ` S ) y ) .x. x ) = ( r .x. ( y .x. x ) ) /\ ( ( 1r ` S ) .x. x ) = x ) ) ) <-> ( ( 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 ) ) ) ) ) ) )
145 6 17 144 3bitri 
 |-  ( 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 ) ) ) ) ) ) )