Step |
Hyp |
Ref |
Expression |
1 |
|
gsumzmhm.b |
|- B = ( Base ` G ) |
2 |
|
gsumzmhm.z |
|- Z = ( Cntz ` G ) |
3 |
|
gsumzmhm.g |
|- ( ph -> G e. Mnd ) |
4 |
|
gsumzmhm.h |
|- ( ph -> H e. Mnd ) |
5 |
|
gsumzmhm.a |
|- ( ph -> A e. V ) |
6 |
|
gsumzmhm.k |
|- ( ph -> K e. ( G MndHom H ) ) |
7 |
|
gsumzmhm.f |
|- ( ph -> F : A --> B ) |
8 |
|
gsumzmhm.c |
|- ( ph -> ran F C_ ( Z ` ran F ) ) |
9 |
|
gsumzmhm.0 |
|- .0. = ( 0g ` G ) |
10 |
|
gsumzmhm.w |
|- ( ph -> F finSupp .0. ) |
11 |
|
eqid |
|- ( 0g ` H ) = ( 0g ` H ) |
12 |
11
|
gsumz |
|- ( ( H e. Mnd /\ A e. V ) -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( 0g ` H ) ) |
13 |
4 5 12
|
syl2anc |
|- ( ph -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( 0g ` H ) ) |
14 |
13
|
adantr |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( 0g ` H ) ) |
15 |
9 11
|
mhm0 |
|- ( K e. ( G MndHom H ) -> ( K ` .0. ) = ( 0g ` H ) ) |
16 |
6 15
|
syl |
|- ( ph -> ( K ` .0. ) = ( 0g ` H ) ) |
17 |
16
|
adantr |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K ` .0. ) = ( 0g ` H ) ) |
18 |
14 17
|
eqtr4d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( k e. A |-> ( 0g ` H ) ) ) = ( K ` .0. ) ) |
19 |
1 9
|
mndidcl |
|- ( G e. Mnd -> .0. e. B ) |
20 |
3 19
|
syl |
|- ( ph -> .0. e. B ) |
21 |
20
|
ad2antrr |
|- ( ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) /\ k e. A ) -> .0. e. B ) |
22 |
9
|
fvexi |
|- .0. e. _V |
23 |
22
|
a1i |
|- ( ph -> .0. e. _V ) |
24 |
7 5
|
fexd |
|- ( ph -> F e. _V ) |
25 |
|
suppimacnv |
|- ( ( F e. _V /\ .0. e. _V ) -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
26 |
24 23 25
|
syl2anc |
|- ( ph -> ( F supp .0. ) = ( `' F " ( _V \ { .0. } ) ) ) |
27 |
|
ssid |
|- ( `' F " ( _V \ { .0. } ) ) C_ ( `' F " ( _V \ { .0. } ) ) |
28 |
26 27
|
eqsstrdi |
|- ( ph -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) |
29 |
7 5 23 28
|
gsumcllem |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> F = ( k e. A |-> .0. ) ) |
30 |
|
eqid |
|- ( Base ` H ) = ( Base ` H ) |
31 |
1 30
|
mhmf |
|- ( K e. ( G MndHom H ) -> K : B --> ( Base ` H ) ) |
32 |
6 31
|
syl |
|- ( ph -> K : B --> ( Base ` H ) ) |
33 |
32
|
feqmptd |
|- ( ph -> K = ( x e. B |-> ( K ` x ) ) ) |
34 |
33
|
adantr |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> K = ( x e. B |-> ( K ` x ) ) ) |
35 |
|
fveq2 |
|- ( x = .0. -> ( K ` x ) = ( K ` .0. ) ) |
36 |
21 29 34 35
|
fmptco |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K o. F ) = ( k e. A |-> ( K ` .0. ) ) ) |
37 |
16
|
mpteq2dv |
|- ( ph -> ( k e. A |-> ( K ` .0. ) ) = ( k e. A |-> ( 0g ` H ) ) ) |
38 |
37
|
adantr |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( k e. A |-> ( K ` .0. ) ) = ( k e. A |-> ( 0g ` H ) ) ) |
39 |
36 38
|
eqtrd |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K o. F ) = ( k e. A |-> ( 0g ` H ) ) ) |
40 |
39
|
oveq2d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( K o. F ) ) = ( H gsum ( k e. A |-> ( 0g ` H ) ) ) ) |
41 |
29
|
oveq2d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum F ) = ( G gsum ( k e. A |-> .0. ) ) ) |
42 |
9
|
gsumz |
|- ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
43 |
3 5 42
|
syl2anc |
|- ( ph -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
44 |
43
|
adantr |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum ( k e. A |-> .0. ) ) = .0. ) |
45 |
41 44
|
eqtrd |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( G gsum F ) = .0. ) |
46 |
45
|
fveq2d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( K ` ( G gsum F ) ) = ( K ` .0. ) ) |
47 |
18 40 46
|
3eqtr4d |
|- ( ( ph /\ ( `' F " ( _V \ { .0. } ) ) = (/) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) |
48 |
47
|
ex |
|- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) ) |
49 |
3
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> G e. Mnd ) |
50 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
51 |
1 50
|
mndcl |
|- ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B ) |
52 |
51
|
3expb |
|- ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B ) |
53 |
49 52
|
sylan |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B ) |
54 |
|
f1of1 |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) ) |
55 |
54
|
ad2antll |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) ) |
56 |
|
cnvimass |
|- ( `' F " ( _V \ { .0. } ) ) C_ dom F |
57 |
7
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> F : A --> B ) |
58 |
56 57
|
fssdm |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( `' F " ( _V \ { .0. } ) ) C_ A ) |
59 |
|
f1ss |
|- ( ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> ( `' F " ( _V \ { .0. } ) ) /\ ( `' F " ( _V \ { .0. } ) ) C_ A ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A ) |
60 |
55 58 59
|
syl2anc |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A ) |
61 |
|
f1f |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-> A -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) |
62 |
60 61
|
syl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) |
63 |
|
fco |
|- ( ( F : A --> B /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> A ) -> ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> B ) |
64 |
7 62 63
|
syl2an2r |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> B ) |
65 |
64
|
ffvelrnda |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( ( F o. f ) ` x ) e. B ) |
66 |
|
simprl |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) |
67 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
68 |
66 67
|
eleqtrdi |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. ( ZZ>= ` 1 ) ) |
69 |
6
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> K e. ( G MndHom H ) ) |
70 |
|
eqid |
|- ( +g ` H ) = ( +g ` H ) |
71 |
1 50 70
|
mhmlin |
|- ( ( K e. ( G MndHom H ) /\ x e. B /\ y e. B ) -> ( K ` ( x ( +g ` G ) y ) ) = ( ( K ` x ) ( +g ` H ) ( K ` y ) ) ) |
72 |
71
|
3expb |
|- ( ( K e. ( G MndHom H ) /\ ( x e. B /\ y e. B ) ) -> ( K ` ( x ( +g ` G ) y ) ) = ( ( K ` x ) ( +g ` H ) ( K ` y ) ) ) |
73 |
69 72
|
sylan |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ ( x e. B /\ y e. B ) ) -> ( K ` ( x ( +g ` G ) y ) ) = ( ( K ` x ) ( +g ` H ) ( K ` y ) ) ) |
74 |
|
coass |
|- ( ( K o. F ) o. f ) = ( K o. ( F o. f ) ) |
75 |
74
|
fveq1i |
|- ( ( ( K o. F ) o. f ) ` x ) = ( ( K o. ( F o. f ) ) ` x ) |
76 |
|
fvco3 |
|- ( ( ( F o. f ) : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) --> B /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( ( K o. ( F o. f ) ) ` x ) = ( K ` ( ( F o. f ) ` x ) ) ) |
77 |
64 76
|
sylan |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( ( K o. ( F o. f ) ) ` x ) = ( K ` ( ( F o. f ) ` x ) ) ) |
78 |
75 77
|
eqtr2id |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) -> ( K ` ( ( F o. f ) ` x ) ) = ( ( ( K o. F ) o. f ) ` x ) ) |
79 |
53 65 68 73 78
|
seqhomo |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) = ( seq 1 ( ( +g ` H ) , ( ( K o. F ) o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) |
80 |
5
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> A e. V ) |
81 |
8
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran F C_ ( Z ` ran F ) ) |
82 |
28
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ( `' F " ( _V \ { .0. } ) ) ) |
83 |
|
f1ofo |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) ) |
84 |
|
forn |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) ) |
85 |
83 84
|
syl |
|- ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) ) |
86 |
85
|
ad2antll |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran f = ( `' F " ( _V \ { .0. } ) ) ) |
87 |
82 86
|
sseqtrrd |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F supp .0. ) C_ ran f ) |
88 |
|
eqid |
|- ( ( F o. f ) supp .0. ) = ( ( F o. f ) supp .0. ) |
89 |
1 9 50 2 49 80 57 81 66 60 87 88
|
gsumval3 |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( G gsum F ) = ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) |
90 |
89
|
fveq2d |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` ( G gsum F ) ) = ( K ` ( seq 1 ( ( +g ` G ) , ( F o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) ) |
91 |
|
eqid |
|- ( Cntz ` H ) = ( Cntz ` H ) |
92 |
4
|
adantr |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> H e. Mnd ) |
93 |
|
fco |
|- ( ( K : B --> ( Base ` H ) /\ F : A --> B ) -> ( K o. F ) : A --> ( Base ` H ) ) |
94 |
32 57 93
|
syl2an2r |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K o. F ) : A --> ( Base ` H ) ) |
95 |
2 91
|
cntzmhm2 |
|- ( ( K e. ( G MndHom H ) /\ ran F C_ ( Z ` ran F ) ) -> ( K " ran F ) C_ ( ( Cntz ` H ) ` ( K " ran F ) ) ) |
96 |
6 81 95
|
syl2an2r |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K " ran F ) C_ ( ( Cntz ` H ) ` ( K " ran F ) ) ) |
97 |
|
rnco2 |
|- ran ( K o. F ) = ( K " ran F ) |
98 |
97
|
fveq2i |
|- ( ( Cntz ` H ) ` ran ( K o. F ) ) = ( ( Cntz ` H ) ` ( K " ran F ) ) |
99 |
96 97 98
|
3sstr4g |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ran ( K o. F ) C_ ( ( Cntz ` H ) ` ran ( K o. F ) ) ) |
100 |
|
eldifi |
|- ( x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) -> x e. A ) |
101 |
|
fvco3 |
|- ( ( F : A --> B /\ x e. A ) -> ( ( K o. F ) ` x ) = ( K ` ( F ` x ) ) ) |
102 |
57 100 101
|
syl2an |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) ` x ) = ( K ` ( F ` x ) ) ) |
103 |
22
|
a1i |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> .0. e. _V ) |
104 |
57 82 80 103
|
suppssr |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( F ` x ) = .0. ) |
105 |
104
|
fveq2d |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` ( F ` x ) ) = ( K ` .0. ) ) |
106 |
16
|
ad2antrr |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( K ` .0. ) = ( 0g ` H ) ) |
107 |
102 105 106
|
3eqtrd |
|- ( ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) /\ x e. ( A \ ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) ` x ) = ( 0g ` H ) ) |
108 |
94 107
|
suppss |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) supp ( 0g ` H ) ) C_ ( `' F " ( _V \ { .0. } ) ) ) |
109 |
108 86
|
sseqtrrd |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( ( K o. F ) supp ( 0g ` H ) ) C_ ran f ) |
110 |
|
eqid |
|- ( ( ( K o. F ) o. f ) supp ( 0g ` H ) ) = ( ( ( K o. F ) o. f ) supp ( 0g ` H ) ) |
111 |
30 11 70 91 92 80 94 99 66 60 109 110
|
gsumval3 |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( H gsum ( K o. F ) ) = ( seq 1 ( ( +g ` H ) , ( ( K o. F ) o. f ) ) ` ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) ) |
112 |
79 90 111
|
3eqtr4rd |
|- ( ( ph /\ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) |
113 |
112
|
expr |
|- ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) ) |
114 |
113
|
exlimdv |
|- ( ( ph /\ ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN ) -> ( E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) ) |
115 |
114
|
expimpd |
|- ( ph -> ( ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) ) |
116 |
10
|
fsuppimpd |
|- ( ph -> ( F supp .0. ) e. Fin ) |
117 |
26 116
|
eqeltrrd |
|- ( ph -> ( `' F " ( _V \ { .0. } ) ) e. Fin ) |
118 |
|
fz1f1o |
|- ( ( `' F " ( _V \ { .0. } ) ) e. Fin -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) ) |
119 |
117 118
|
syl |
|- ( ph -> ( ( `' F " ( _V \ { .0. } ) ) = (/) \/ ( ( # ` ( `' F " ( _V \ { .0. } ) ) ) e. NN /\ E. f f : ( 1 ... ( # ` ( `' F " ( _V \ { .0. } ) ) ) ) -1-1-onto-> ( `' F " ( _V \ { .0. } ) ) ) ) ) |
120 |
48 115 119
|
mpjaod |
|- ( ph -> ( H gsum ( K o. F ) ) = ( K ` ( G gsum F ) ) ) |