Step |
Hyp |
Ref |
Expression |
1 |
|
gsumval.b |
|- B = ( Base ` G ) |
2 |
|
gsumval.z |
|- .0. = ( 0g ` G ) |
3 |
|
gsumval.p |
|- .+ = ( +g ` G ) |
4 |
|
gsumval.o |
|- O = { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) } |
5 |
|
gsumval.w |
|- ( ph -> W = ( `' F " ( _V \ O ) ) ) |
6 |
|
gsumval.g |
|- ( ph -> G e. V ) |
7 |
|
gsumvalx.f |
|- ( ph -> F e. X ) |
8 |
|
gsumvalx.a |
|- ( ph -> dom F = A ) |
9 |
|
df-gsum |
|- gsum = ( w e. _V , g e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) ) |
10 |
9
|
a1i |
|- ( ph -> gsum = ( w e. _V , g e. _V |-> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) ) ) |
11 |
|
simprl |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> w = G ) |
12 |
11
|
fveq2d |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( Base ` w ) = ( Base ` G ) ) |
13 |
12 1
|
eqtr4di |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( Base ` w ) = B ) |
14 |
11
|
fveq2d |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( +g ` w ) = ( +g ` G ) ) |
15 |
14 3
|
eqtr4di |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( +g ` w ) = .+ ) |
16 |
15
|
oveqd |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( x ( +g ` w ) y ) = ( x .+ y ) ) |
17 |
16
|
eqeq1d |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( x ( +g ` w ) y ) = y <-> ( x .+ y ) = y ) ) |
18 |
15
|
oveqd |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( y ( +g ` w ) x ) = ( y .+ x ) ) |
19 |
18
|
eqeq1d |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( y ( +g ` w ) x ) = y <-> ( y .+ x ) = y ) ) |
20 |
17 19
|
anbi12d |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) <-> ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) |
21 |
13 20
|
raleqbidv |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> ( A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) |
22 |
13 21
|
rabeqbidv |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } ) |
23 |
|
oveq2 |
|- ( t = y -> ( s .+ t ) = ( s .+ y ) ) |
24 |
|
id |
|- ( t = y -> t = y ) |
25 |
23 24
|
eqeq12d |
|- ( t = y -> ( ( s .+ t ) = t <-> ( s .+ y ) = y ) ) |
26 |
|
oveq1 |
|- ( t = y -> ( t .+ s ) = ( y .+ s ) ) |
27 |
26 24
|
eqeq12d |
|- ( t = y -> ( ( t .+ s ) = t <-> ( y .+ s ) = y ) ) |
28 |
25 27
|
anbi12d |
|- ( t = y -> ( ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> ( ( s .+ y ) = y /\ ( y .+ s ) = y ) ) ) |
29 |
28
|
cbvralvw |
|- ( A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> A. y e. B ( ( s .+ y ) = y /\ ( y .+ s ) = y ) ) |
30 |
|
oveq1 |
|- ( s = x -> ( s .+ y ) = ( x .+ y ) ) |
31 |
30
|
eqeq1d |
|- ( s = x -> ( ( s .+ y ) = y <-> ( x .+ y ) = y ) ) |
32 |
31
|
ovanraleqv |
|- ( s = x -> ( A. y e. B ( ( s .+ y ) = y /\ ( y .+ s ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) |
33 |
29 32
|
syl5bb |
|- ( s = x -> ( A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) |
34 |
33
|
cbvrabv |
|- { s e. B | A. t e. B ( ( s .+ t ) = t /\ ( t .+ s ) = t ) } = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } |
35 |
4 34
|
eqtri |
|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } |
36 |
22 35
|
eqtr4di |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } = O ) |
37 |
36
|
csbeq1d |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = [_ O / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) ) |
38 |
1
|
fvexi |
|- B e. _V |
39 |
4 38
|
rabex2 |
|- O e. _V |
40 |
39
|
a1i |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> O e. _V ) |
41 |
|
simplrr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> g = F ) |
42 |
41
|
rneqd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ran g = ran F ) |
43 |
|
simpr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> o = O ) |
44 |
42 43
|
sseq12d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( ran g C_ o <-> ran F C_ O ) ) |
45 |
11
|
adantr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> w = G ) |
46 |
45
|
fveq2d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( 0g ` w ) = ( 0g ` G ) ) |
47 |
46 2
|
eqtr4di |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( 0g ` w ) = .0. ) |
48 |
41
|
dmeqd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom g = dom F ) |
49 |
8
|
ad2antrr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom F = A ) |
50 |
48 49
|
eqtrd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> dom g = A ) |
51 |
50
|
eleq1d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( dom g e. ran ... <-> A e. ran ... ) ) |
52 |
50
|
eqeq1d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( dom g = ( m ... n ) <-> A = ( m ... n ) ) ) |
53 |
15
|
adantr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( +g ` w ) = .+ ) |
54 |
53
|
seqeq2d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( ( +g ` w ) , g ) = seq m ( .+ , g ) ) |
55 |
41
|
seqeq3d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( .+ , g ) = seq m ( .+ , F ) ) |
56 |
54 55
|
eqtrd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq m ( ( +g ` w ) , g ) = seq m ( .+ , F ) ) |
57 |
56
|
fveq1d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( seq m ( ( +g ` w ) , g ) ` n ) = ( seq m ( .+ , F ) ` n ) ) |
58 |
57
|
eqeq2d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( x = ( seq m ( ( +g ` w ) , g ) ` n ) <-> x = ( seq m ( .+ , F ) ` n ) ) ) |
59 |
52 58
|
anbi12d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) <-> ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) |
60 |
59
|
rexbidv |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) <-> E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) |
61 |
60
|
exbidv |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) <-> E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) |
62 |
61
|
iotabidv |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) = ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) ) |
63 |
43
|
difeq2d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( _V \ o ) = ( _V \ O ) ) |
64 |
63
|
imaeq2d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' F " ( _V \ o ) ) = ( `' F " ( _V \ O ) ) ) |
65 |
41
|
cnveqd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> `' g = `' F ) |
66 |
65
|
imaeq1d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' g " ( _V \ o ) ) = ( `' F " ( _V \ o ) ) ) |
67 |
5
|
ad2antrr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> W = ( `' F " ( _V \ O ) ) ) |
68 |
64 66 67
|
3eqtr4d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( `' g " ( _V \ o ) ) = W ) |
69 |
68
|
sbceq1d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> [. W / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) |
70 |
|
cnvexg |
|- ( F e. X -> `' F e. _V ) |
71 |
|
imaexg |
|- ( `' F e. _V -> ( `' F " ( _V \ O ) ) e. _V ) |
72 |
7 70 71
|
3syl |
|- ( ph -> ( `' F " ( _V \ O ) ) e. _V ) |
73 |
5 72
|
eqeltrd |
|- ( ph -> W e. _V ) |
74 |
73
|
ad2antrr |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> W e. _V ) |
75 |
|
fveq2 |
|- ( y = W -> ( # ` y ) = ( # ` W ) ) |
76 |
75
|
adantl |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( # ` y ) = ( # ` W ) ) |
77 |
76
|
oveq2d |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( 1 ... ( # ` y ) ) = ( 1 ... ( # ` W ) ) ) |
78 |
77
|
f1oeq2d |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> y ) ) |
79 |
|
f1oeq3 |
|- ( y = W -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) |
80 |
79
|
adantl |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) |
81 |
78 80
|
bitrd |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y <-> f : ( 1 ... ( # ` W ) ) -1-1-onto-> W ) ) |
82 |
53
|
seqeq2d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( g o. f ) ) ) |
83 |
41
|
coeq1d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( g o. f ) = ( F o. f ) ) |
84 |
83
|
seqeq3d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( .+ , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) ) |
85 |
82 84
|
eqtrd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) ) |
86 |
85
|
adantr |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> seq 1 ( ( +g ` w ) , ( g o. f ) ) = seq 1 ( .+ , ( F o. f ) ) ) |
87 |
86 76
|
fveq12d |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) |
88 |
87
|
eqeq2d |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) <-> x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) |
89 |
81 88
|
anbi12d |
|- ( ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) /\ y = W ) -> ( ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |
90 |
74 89
|
sbcied |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( [. W / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |
91 |
69 90
|
bitrd |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |
92 |
91
|
exbidv |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) <-> E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |
93 |
92
|
iotabidv |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) = ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) |
94 |
51 62 93
|
ifbieq12d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) = if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) |
95 |
44 47 94
|
ifbieq12d |
|- ( ( ( ph /\ ( w = G /\ g = F ) ) /\ o = O ) -> if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) ) |
96 |
40 95
|
csbied |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> [_ O / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) ) |
97 |
37 96
|
eqtrd |
|- ( ( ph /\ ( w = G /\ g = F ) ) -> [_ { x e. ( Base ` w ) | A. y e. ( Base ` w ) ( ( x ( +g ` w ) y ) = y /\ ( y ( +g ` w ) x ) = y ) } / o ]_ if ( ran g C_ o , ( 0g ` w ) , if ( dom g e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( dom g = ( m ... n ) /\ x = ( seq m ( ( +g ` w ) , g ) ` n ) ) ) , ( iota x E. f [. ( `' g " ( _V \ o ) ) / y ]. ( f : ( 1 ... ( # ` y ) ) -1-1-onto-> y /\ x = ( seq 1 ( ( +g ` w ) , ( g o. f ) ) ` ( # ` y ) ) ) ) ) ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) ) |
98 |
6
|
elexd |
|- ( ph -> G e. _V ) |
99 |
7
|
elexd |
|- ( ph -> F e. _V ) |
100 |
2
|
fvexi |
|- .0. e. _V |
101 |
|
iotaex |
|- ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) e. _V |
102 |
|
iotaex |
|- ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) e. _V |
103 |
101 102
|
ifex |
|- if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) e. _V |
104 |
100 103
|
ifex |
|- if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) e. _V |
105 |
104
|
a1i |
|- ( ph -> if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) e. _V ) |
106 |
10 97 98 99 105
|
ovmpod |
|- ( ph -> ( G gsum F ) = if ( ran F C_ O , .0. , if ( A e. ran ... , ( iota x E. m E. n e. ( ZZ>= ` m ) ( A = ( m ... n ) /\ x = ( seq m ( .+ , F ) ` n ) ) ) , ( iota x E. f ( f : ( 1 ... ( # ` W ) ) -1-1-onto-> W /\ x = ( seq 1 ( .+ , ( F o. f ) ) ` ( # ` W ) ) ) ) ) ) ) |