MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isclmp Structured version   Visualization version   Unicode version
Theorem isclmp 22897
Description: The predicate "is a subcomplex module." (Contributed by NM, 31-May-2008.) (Revised by AV, 4-Oct-2021.)
Hypotheses
Ref Expression
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
Ref Expression
isclmp |- ( W e. CMod <-> ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ 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 ) ) ) ) ) ) )
Distinct variable groups:   x, K, y, z   x, S, y, z   x, V, y, z   x, W, y, z   x, .+ , y, z   x, .x. , y, z
Proof of Theorem isclmp
Dummy variable r is distinct from all other variables.
StepHypRef Expression
1 isclmp.s . . 3 |- S = (Scalar ` W )
2 isclmp.k . . 3 |- K = ( Base ` S )
31, 2isclm 22864 . 2 |- ( W e. CMod <-> ( W e. LMod /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) )
4 isclmp.v . . . . 5 |- V = ( Base ` W )
5 isclmp.a . . . . 5 |- .+ = ( +g ` W )
6 isclmp.t . . . . 5 |- .x. = ( .s ` W )
7 eqid 2622 . . . . 5 |- ( +g ` S ) = ( +g ` S )
8 eqid 2622 . . . . 5 |- ( .r ` S ) = ( .r ` S )
9 eqid 2622 . . . . 5 |- ( 1r ` S ) = ( 1r ` S )
104, 5, 6, 1, 2, 7, 8, 9islmod 18867 . . . 4 |- ( 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 ) ) ) )
11103anbi1i 1253 . . 3 |- ( ( W e. LMod /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) <-> ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) )
12 3anass 1042 . . . 4 |- ( ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) <-> ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) )
13 df-3an 1039 . . . . 5 |- ( ( 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 ) ) ) )
1413anbi1i 731 . . . 4 |- ( ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) <-> ( ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) )
1512, 14bitri 264 . . 3 |- ( ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) <-> ( ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) )
16 an32 839 . . 3 |- ( ( ( ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) <-> ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) /\ 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 ) ) ) )
1711, 15, 163bitri 286 . 2 |- ( ( W e. LMod /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) <-> ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) /\ 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 839 . . . . 5 |- ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) <-> ( ( W e. Grp /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) /\ S e. Ring ) )
19 3anass 1042 . . . . . . 7 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) <-> ( W e. Grp /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) )
2019bicomi 214 . . . . . 6 |- ( ( W e. Grp /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) <-> ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) )
2120anbi1i 731 . . . . 5 |- ( ( ( W e. Grp /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) /\ S e. Ring ) <-> ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ S e. Ring ) )
2218, 21bitri 264 . . . 4 |- ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) <-> ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ S e. Ring ) )
2322anbi1i 731 . . 3 |- ( ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) /\ 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ 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 681 . . 3 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 1039 . . . . . . . . . . 11 |- ( ( ( 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 466 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
2725, 26anbi12i 733 . . . . . . . . . 10 |- ( ( ( ( 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 865 . . . . . . . . . 10 |- ( ( ( ( ( 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 839 . . . . . . . . . . . 12 |- ( ( ( ( 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 466 . . . . . . . . . . . . 13 |- ( ( ( y .x. x ) e. V /\ ( ( 1r ` S ) .x. x ) = x ) <-> ( ( ( 1r ` S ) .x. x ) = x /\ ( y .x. x ) e. V ) )
3130anbi1i 731 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) )
3229, 31bitri 264 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) )
3332anbi1i 731 . . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) ) ) )
3427, 28, 333bitri 286 . . . . . . . . 9 |- ( ( ( ( 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 6191 . . . . . . . . . . . . . . . . . 18 |- ( S = (ℂfld ↾s K ) -> ( 1r ` S ) = ( 1r ` (ℂfld ↾s K ) ) )
36 eqid 2622 . . . . . . . . . . . . . . . . . . . 20 |- (ℂfld ↾s K ) = (ℂfld ↾s K )
37 eqid 2622 . . . . . . . . . . . . . . . . . . . 20 |- ( 1r ` ℂfld ) = ( 1r ` ℂfld )
3836, 37subrg1 18790 . . . . . . . . . . . . . . . . . . 19 |- ( K e. (SubRing ` ℂfld ) -> ( 1r ` ℂfld ) = ( 1r ` (ℂfld ↾s K ) ) )
3938eqcomd 2628 . . . . . . . . . . . . . . . . . 18 |- ( K e. (SubRing ` ℂfld ) -> ( 1r ` (ℂfld ↾s K ) ) = ( 1r ` ℂfld ) )
4035, 39sylan9eq 2676 . . . . . . . . . . . . . . . . 17 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 1r ` S ) = ( 1r ` ℂfld ) )
41 cnfld1 19771 . . . . . . . . . . . . . . . . 17 |- 1 = ( 1r ` ℂfld )
4240, 41syl6eqr 2674 . . . . . . . . . . . . . . . 16 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 1r ` S ) = 1 )
4342oveq1d 6665 . . . . . . . . . . . . . . 15 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( ( 1r ` S ) .x. x ) = ( 1 .x. x ) )
4443eqeq1d 2624 . . . . . . . . . . . . . 14 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( ( ( 1r ` S ) .x. x ) = x <-> ( 1 .x. x ) = x ) )
45443adant1 1079 . . . . . . . . . . . . 13 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( ( ( 1r ` S ) .x. x ) = x <-> ( 1 .x. x ) = x ) )
4645ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( ( 1r ` S ) .x. x ) = x <-> ( 1 .x. x ) = x ) )
4746anbi1d 741 . . . . . . . . . . 11 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 ) ) )
4847anbi1d 741 . . . . . . . . . 10 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 2622 . . . . . . . . . . . . . . . . . . 19 |- ( +g ` ℂfld ) = ( +g ` ℂfld )
5036, 49ressplusg 15993 . . . . . . . . . . . . . . . . . 18 |- ( K e. (SubRing ` ℂfld ) -> ( +g ` ℂfld ) = ( +g ` (ℂfld ↾s K ) ) )
5150adantl 482 . . . . . . . . . . . . . . . . 17 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( +g ` ℂfld ) = ( +g ` (ℂfld ↾s K ) ) )
52 cnfldadd 19751 . . . . . . . . . . . . . . . . . 18 |- + = ( +g ` ℂfld )
5352a1i 11 . . . . . . . . . . . . . . . . 17 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> + = ( +g ` ℂfld ) )
54 fveq2 6191 . . . . . . . . . . . . . . . . . 18 |- ( S = (ℂfld ↾s K ) -> ( +g ` S ) = ( +g ` (ℂfld ↾s K ) ) )
5554adantr 481 . . . . . . . . . . . . . . . . 17 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( +g ` S ) = ( +g ` (ℂfld ↾s K ) ) )
5651, 53, 553eqtr4rd 2667 . . . . . . . . . . . . . . . 16 |- ( ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( +g ` S ) = + )
57563adant1 1079 . . . . . . . . . . . . . . 15 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( +g ` S ) = + )
5857oveqd 6667 . . . . . . . . . . . . . 14 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( r ( +g ` S ) y ) = ( r + y ) )
5958ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( r ( +g ` S ) y ) = ( r + y ) )
6059oveq1d 6665 . . . . . . . . . . . 12 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( r ( +g ` S ) y ) .x. x ) = ( ( r + y ) .x. x ) )
6160eqeq1d 2624 . . . . . . . . . . 11 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 2622 . . . . . . . . . . . . . . . . . 18 |- ( .r ` ℂfld ) = ( .r ` ℂfld )
6336, 62ressmulr 16006 . . . . . . . . . . . . . . . . 17 |- ( K e. (SubRing ` ℂfld ) -> ( .r ` ℂfld ) = ( .r ` (ℂfld ↾s K ) ) )
64633ad2ant3 1084 . . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( .r ` ℂfld ) = ( .r ` (ℂfld ↾s K ) ) )
65 cnfldmul 19752 . . . . . . . . . . . . . . . . 17 |- x. = ( .r ` ℂfld )
6665a1i 11 . . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> x. = ( .r ` ℂfld ) )
67 fveq2 6191 . . . . . . . . . . . . . . . . 17 |- ( S = (ℂfld ↾s K ) -> ( .r ` S ) = ( .r ` (ℂfld ↾s K ) ) )
68673ad2ant2 1083 . . . . . . . . . . . . . . . 16 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( .r ` S ) = ( .r ` (ℂfld ↾s K ) ) )
6964, 66, 683eqtr4rd 2667 . . . . . . . . . . . . . . 15 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( .r ` S ) = x. )
7069oveqd 6667 . . . . . . . . . . . . . 14 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( r ( .r ` S ) y ) = ( r x. y ) )
7170ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( r ( .r ` S ) y ) = ( r x. y ) )
7271oveq1d 6665 . . . . . . . . . . . 12 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( r e. K /\ y e. K ) ) /\ ( z e. V /\ x e. V ) ) -> ( ( r ( .r ` S ) y ) .x. x ) = ( ( r x. y ) .x. x ) )
7372eqeq1d 2624 . . . . . . . . . . 11 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 ) ) ) )
7461, 73anbi12d 747 . . . . . . . . . 10 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 ) ) ) ) )
7548, 74anbi12d 747 . . . . . . . . 9 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 ) ) ) ) ) )
7634, 75syl5bb 272 . . . . . . . 8 |- ( ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 ) ) ) ) ) )
77762ralbidva 2988 . . . . . . 7 |- ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 ) ) ) ) ) )
78772ralbidva 2988 . . . . . 6 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 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 ralcom 3098 . . . . . . . . . . 11 |- ( 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. 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 ) ) ) ) )
8079ralbii 2980 . . . . . . . . . 10 |- ( 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. y e. K A. x e. V 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 3098 . . . . . . . . . 10 |- ( A. y e. K A. x e. V 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 ( ( ( ( 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 ) ) ) ) )
8280, 81bitri 264 . . . . . . . . 9 |- ( 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 ) ) ) ) )
8382ralbii 2980 . . . . . . . 8 |- ( 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 ) ) ) ) )
84 ralcom 3098 . . . . . . . 8 |- ( 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 ) ) ) ) )
8583, 84bitri 264 . . . . . . 7 |- ( 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 ) ) ) ) )
86 ralcom 3098 . . . . . . . 8 |- ( 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 ) ) ) ) )
8786ralbii 2980 . . . . . . 7 |- ( 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 ) ) ) ) )
88 ralcom 3098 . . . . . . . 8 |- ( 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 ) ) ) ) )
89882ralbii 2981 . . . . . . 7 |- ( 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 ) ) ) ) )
9085, 87, 893bitri 286 . . . . . 6 |- ( 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 ) ) ) ) )
9178, 90syl6bb 276 . . . . 5 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 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 ) ) ) ) ) )
9236subrgring 18783 . . . . . . . 8 |- ( K e. (SubRing ` ℂfld ) -> (ℂfld ↾s K ) e. Ring )
93923ad2ant3 1084 . . . . . . 7 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> (ℂfld ↾s K ) e. Ring )
94 eleq1 2689 . . . . . . . 8 |- ( S = (ℂfld ↾s K ) -> ( S e. Ring <-> (ℂfld ↾s K ) e. Ring ) )
95943ad2ant2 1083 . . . . . . 7 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( S e. Ring <-> (ℂfld ↾s K ) e. Ring ) )
9693, 95mpbird 247 . . . . . 6 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> S e. Ring )
9796biantrurd 529 . . . . 5 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 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 ) ) ) ) )
984grpbn0 17451 . . . . . . . 8 |- ( W e. Grp -> V =/= (/) )
99983ad2ant1 1082 . . . . . . 7 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> V =/= (/) )
10037subrg1cl 18788 . . . . . . . . 9 |- ( K e. (SubRing ` ℂfld ) -> ( 1r ` ℂfld ) e. K )
101 ne0i 3921 . . . . . . . . 9 |- ( ( 1r ` ℂfld ) e. K -> K =/= (/) )
102100, 101syl 17 . . . . . . . 8 |- ( K e. (SubRing ` ℂfld ) -> K =/= (/) )
1031023ad2ant3 1084 . . . . . . 7 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> K =/= (/) )
104 ancom 466 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 ) ) )
105104anbi1i 731 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) ) ) ) )
106105a1i 11 . . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) ) ) )
107106ralbidv 2986 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) )
108 r19.28zv 4066 . . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) )
109108adantl 482 . . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) ) )
110107, 109bitrd 268 . . . . . . . . . . . . 13 |- ( ( 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 ) ) ) ) ) )
111 anass 681 . . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) ) ) ) ) )
112 anass 681 . . . . . . . . . . . . . . 15 |- ( ( ( ( 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 ) ) ) ) ) )
113112anbi2i 730 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) ) ) ) )
114 ancom 466 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) )
115111, 113, 1143bitri 286 . . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
116110, 115syl6bb 276 . . . . . . . . . . . 12 |- ( ( 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 ) ) ) ) )
117116ralbidv 2986 . . . . . . . . . . 11 |- ( ( 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 ) ) ) ) )
118 r19.28zv 4066 . . . . . . . . . . . 12 |- ( 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 ) ) ) ) )
119118adantr 481 . . . . . . . . . . 11 |- ( ( 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 ) ) ) ) )
120117, 119bitrd 268 . . . . . . . . . 10 |- ( ( 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 ) ) ) ) )
121 anass 681 . . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) ) )
122 oveq1 6657 . . . . . . . . . . . . . . . . . . 19 |- ( z = r -> ( z + y ) = ( r + y ) )
123122oveq1d 6665 . . . . . . . . . . . . . . . . . 18 |- ( z = r -> ( ( z + y ) .x. x ) = ( ( r + y ) .x. x ) )
124 oveq1 6657 . . . . . . . . . . . . . . . . . . 19 |- ( z = r -> ( z .x. x ) = ( r .x. x ) )
125124oveq1d 6665 . . . . . . . . . . . . . . . . . 18 |- ( z = r -> ( ( z .x. x ) .+ ( y .x. x ) ) = ( ( r .x. x ) .+ ( y .x. x ) ) )
126123, 125eqeq12d 2637 . . . . . . . . . . . . . . . . 17 |- ( z = r -> ( ( ( z + y ) .x. x ) = ( ( z .x. x ) .+ ( y .x. x ) ) <-> ( ( r + y ) .x. x ) = ( ( r .x. x ) .+ ( y .x. x ) ) ) )
127 oveq1 6657 . . . . . . . . . . . . . . . . . . 19 |- ( z = r -> ( z x. y ) = ( r x. y ) )
128127oveq1d 6665 . . . . . . . . . . . . . . . . . 18 |- ( z = r -> ( ( z x. y ) .x. x ) = ( ( r x. y ) .x. x ) )
129 oveq1 6657 . . . . . . . . . . . . . . . . . 18 |- ( z = r -> ( z .x. ( y .x. x ) ) = ( r .x. ( y .x. x ) ) )
130128, 129eqeq12d 2637 . . . . . . . . . . . . . . . . 17 |- ( z = r -> ( ( ( z x. y ) .x. x ) = ( z .x. ( y .x. x ) ) <-> ( ( r x. y ) .x. x ) = ( r .x. ( y .x. x ) ) ) )
131126, 130anbi12d 747 . . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
132131cbvralv 3171 . . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
1331323anbi3i 1255 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) ) )
134 3anan32 1050 . . . . . . . . . . . . . 14 |- ( ( ( 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 ) ) ) )
135133, 134bitri 264 . . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) )
136135bicomi 214 . . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) ) )
137136anbi2i 730 . . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) ) )
138121, 137bitri 264 . . . . . . . . . 10 |- ( ( ( ( 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 ) ) ) ) ) )
139120, 138syl6bb 276 . . . . . . . . 9 |- ( ( 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 ) ) ) ) ) ) )
140139ralbidv 2986 . . . . . . . 8 |- ( ( 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 ) ) ) ) ) ) )
141 r19.28zv 4066 . . . . . . . . 9 |- ( 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 ) ) ) ) ) ) )
142141adantl 482 . . . . . . . 8 |- ( ( 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 ) ) ) ) ) ) )
143140, 142bitrd 268 . . . . . . 7 |- ( ( 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 ) ) ) ) ) ) )
14499, 103, 143syl2anc 693 . . . . . 6 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 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 ) ) ) ) ) ) )
145144ralbidv 2986 . . . . 5 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( 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 ) ) ) ) ) ) )
14691, 97, 1453bitr3d 298 . . . 4 |- ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) -> ( ( 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 ) ) ) ) ) ) )
147146pm5.32i 669 . . 3 |- ( ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ ( 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ 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 ) ) ) ) ) ) )
14823, 24, 1473bitri 286 . 2 |- ( ( ( ( W e. Grp /\ S e. Ring ) /\ ( S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) ) /\ 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 = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ 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 ) ) ) ) ) ) )
1493, 17, 1483bitri 286 1 |- ( W e. CMod <-> ( ( W e. Grp /\ S = (ℂfld ↾s K ) /\ K e. (SubRing ` ℂfld ) ) /\ 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 ) ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   (/)c0 3915   ` cfv 5888  (class class class)co 6650   1c1 9937   + caddc 9939   x. cmul 9941   Basecbs 15857   ↾s cress 15858   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   Grpcgrp 17422   1rcur 18501   Ringcrg 18547  SubRingcsubrg 18776   LModclmod 18863  ℂfldccnfld 19746  CModcclm 22862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-addf 10015  ax-mulf 10016
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-fz 12327  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-0g 16102  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-grp 17425  df-subg 17591  df-cmn 18195  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-subrg 18778  df-lmod 18865  df-cnfld 19747  df-clm 22863
This theorem is referenced by:  isclmi0  22898  iscvsp  22928
  Copyright terms: Public domain W3C validator