Step |
Hyp |
Ref |
Expression |
1 |
|
tmdgsum.j |
|- J = ( TopOpen ` G ) |
2 |
|
tmdgsum.b |
|- B = ( Base ` G ) |
3 |
|
oveq2 |
|- ( w = (/) -> ( B ^m w ) = ( B ^m (/) ) ) |
4 |
3
|
mpteq1d |
|- ( w = (/) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) ) |
5 |
|
xpeq1 |
|- ( w = (/) -> ( w X. { J } ) = ( (/) X. { J } ) ) |
6 |
|
0xp |
|- ( (/) X. { J } ) = (/) |
7 |
5 6
|
eqtrdi |
|- ( w = (/) -> ( w X. { J } ) = (/) ) |
8 |
7
|
fveq2d |
|- ( w = (/) -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` (/) ) ) |
9 |
8
|
oveq1d |
|- ( w = (/) -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` (/) ) Cn J ) ) |
10 |
4 9
|
eleq12d |
|- ( w = (/) -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` (/) ) Cn J ) ) ) |
11 |
10
|
imbi2d |
|- ( w = (/) -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` (/) ) Cn J ) ) ) ) |
12 |
|
oveq2 |
|- ( w = y -> ( B ^m w ) = ( B ^m y ) ) |
13 |
12
|
mpteq1d |
|- ( w = y -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m y ) |-> ( G gsum x ) ) ) |
14 |
|
xpeq1 |
|- ( w = y -> ( w X. { J } ) = ( y X. { J } ) ) |
15 |
14
|
fveq2d |
|- ( w = y -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` ( y X. { J } ) ) ) |
16 |
15
|
oveq1d |
|- ( w = y -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) |
17 |
13 16
|
eleq12d |
|- ( w = y -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) ) |
18 |
17
|
imbi2d |
|- ( w = y -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) ) ) |
19 |
|
oveq2 |
|- ( w = ( y u. { z } ) -> ( B ^m w ) = ( B ^m ( y u. { z } ) ) ) |
20 |
19
|
mpteq1d |
|- ( w = ( y u. { z } ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) ) |
21 |
|
xpeq1 |
|- ( w = ( y u. { z } ) -> ( w X. { J } ) = ( ( y u. { z } ) X. { J } ) ) |
22 |
21
|
fveq2d |
|- ( w = ( y u. { z } ) -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) ) |
23 |
22
|
oveq1d |
|- ( w = ( y u. { z } ) -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
24 |
20 23
|
eleq12d |
|- ( w = ( y u. { z } ) -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) |
25 |
24
|
imbi2d |
|- ( w = ( y u. { z } ) -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) ) |
26 |
|
oveq2 |
|- ( w = A -> ( B ^m w ) = ( B ^m A ) ) |
27 |
26
|
mpteq1d |
|- ( w = A -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) = ( x e. ( B ^m A ) |-> ( G gsum x ) ) ) |
28 |
|
xpeq1 |
|- ( w = A -> ( w X. { J } ) = ( A X. { J } ) ) |
29 |
28
|
fveq2d |
|- ( w = A -> ( Xt_ ` ( w X. { J } ) ) = ( Xt_ ` ( A X. { J } ) ) ) |
30 |
29
|
oveq1d |
|- ( w = A -> ( ( Xt_ ` ( w X. { J } ) ) Cn J ) = ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) |
31 |
27 30
|
eleq12d |
|- ( w = A -> ( ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) <-> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) ) |
32 |
31
|
imbi2d |
|- ( w = A -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m w ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( w X. { J } ) ) Cn J ) ) <-> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) ) ) |
33 |
|
elmapfn |
|- ( x e. ( B ^m (/) ) -> x Fn (/) ) |
34 |
|
fn0 |
|- ( x Fn (/) <-> x = (/) ) |
35 |
33 34
|
sylib |
|- ( x e. ( B ^m (/) ) -> x = (/) ) |
36 |
35
|
oveq2d |
|- ( x e. ( B ^m (/) ) -> ( G gsum x ) = ( G gsum (/) ) ) |
37 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
38 |
37
|
gsum0 |
|- ( G gsum (/) ) = ( 0g ` G ) |
39 |
36 38
|
eqtrdi |
|- ( x e. ( B ^m (/) ) -> ( G gsum x ) = ( 0g ` G ) ) |
40 |
39
|
mpteq2ia |
|- ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) = ( x e. ( B ^m (/) ) |-> ( 0g ` G ) ) |
41 |
|
0ex |
|- (/) e. _V |
42 |
1 2
|
tmdtopon |
|- ( G e. TopMnd -> J e. ( TopOn ` B ) ) |
43 |
42
|
adantl |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> J e. ( TopOn ` B ) ) |
44 |
6
|
fveq2i |
|- ( Xt_ ` ( (/) X. { J } ) ) = ( Xt_ ` (/) ) |
45 |
44
|
eqcomi |
|- ( Xt_ ` (/) ) = ( Xt_ ` ( (/) X. { J } ) ) |
46 |
45
|
pttoponconst |
|- ( ( (/) e. _V /\ J e. ( TopOn ` B ) ) -> ( Xt_ ` (/) ) e. ( TopOn ` ( B ^m (/) ) ) ) |
47 |
41 43 46
|
sylancr |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> ( Xt_ ` (/) ) e. ( TopOn ` ( B ^m (/) ) ) ) |
48 |
|
tmdmnd |
|- ( G e. TopMnd -> G e. Mnd ) |
49 |
48
|
adantl |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> G e. Mnd ) |
50 |
2 37
|
mndidcl |
|- ( G e. Mnd -> ( 0g ` G ) e. B ) |
51 |
49 50
|
syl |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> ( 0g ` G ) e. B ) |
52 |
47 43 51
|
cnmptc |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m (/) ) |-> ( 0g ` G ) ) e. ( ( Xt_ ` (/) ) Cn J ) ) |
53 |
40 52
|
eqeltrid |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m (/) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` (/) ) Cn J ) ) |
54 |
|
oveq2 |
|- ( x = w -> ( G gsum x ) = ( G gsum w ) ) |
55 |
54
|
cbvmptv |
|- ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum w ) ) |
56 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
57 |
|
simpl1l |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> G e. CMnd ) |
58 |
|
simp2l |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> y e. Fin ) |
59 |
|
snfi |
|- { z } e. Fin |
60 |
|
unfi |
|- ( ( y e. Fin /\ { z } e. Fin ) -> ( y u. { z } ) e. Fin ) |
61 |
58 59 60
|
sylancl |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( y u. { z } ) e. Fin ) |
62 |
61
|
adantr |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( y u. { z } ) e. Fin ) |
63 |
|
elmapi |
|- ( w e. ( B ^m ( y u. { z } ) ) -> w : ( y u. { z } ) --> B ) |
64 |
63
|
adantl |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> w : ( y u. { z } ) --> B ) |
65 |
|
fvexd |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( 0g ` G ) e. _V ) |
66 |
64 62 65
|
fdmfifsupp |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> w finSupp ( 0g ` G ) ) |
67 |
|
simpl2r |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> -. z e. y ) |
68 |
|
disjsn |
|- ( ( y i^i { z } ) = (/) <-> -. z e. y ) |
69 |
67 68
|
sylibr |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( y i^i { z } ) = (/) ) |
70 |
|
eqidd |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( y u. { z } ) = ( y u. { z } ) ) |
71 |
2 37 56 57 62 64 66 69 70
|
gsumsplit |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum w ) = ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) |
72 |
71
|
mpteq2dva |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum w ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) ) |
73 |
55 72
|
eqtrid |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) ) |
74 |
|
simp1r |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> G e. TopMnd ) |
75 |
74 42
|
syl |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> J e. ( TopOn ` B ) ) |
76 |
|
eqid |
|- ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) = ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |
77 |
76
|
pttoponconst |
|- ( ( ( y u. { z } ) e. Fin /\ J e. ( TopOn ` B ) ) -> ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) e. ( TopOn ` ( B ^m ( y u. { z } ) ) ) ) |
78 |
61 75 77
|
syl2anc |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) e. ( TopOn ` ( B ^m ( y u. { z } ) ) ) ) |
79 |
|
toponuni |
|- ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) e. ( TopOn ` ( B ^m ( y u. { z } ) ) ) -> ( B ^m ( y u. { z } ) ) = U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) ) |
80 |
78 79
|
syl |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( B ^m ( y u. { z } ) ) = U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) ) |
81 |
80
|
mpteq1d |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w |` y ) ) = ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w |` y ) ) ) |
82 |
|
topontop |
|- ( J e. ( TopOn ` B ) -> J e. Top ) |
83 |
74 42 82
|
3syl |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> J e. Top ) |
84 |
|
fconst6g |
|- ( J e. Top -> ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top ) |
85 |
83 84
|
syl |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top ) |
86 |
|
ssun1 |
|- y C_ ( y u. { z } ) |
87 |
86
|
a1i |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> y C_ ( y u. { z } ) ) |
88 |
|
eqid |
|- U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) = U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |
89 |
|
xpssres |
|- ( y C_ ( y u. { z } ) -> ( ( ( y u. { z } ) X. { J } ) |` y ) = ( y X. { J } ) ) |
90 |
86 89
|
ax-mp |
|- ( ( ( y u. { z } ) X. { J } ) |` y ) = ( y X. { J } ) |
91 |
90
|
eqcomi |
|- ( y X. { J } ) = ( ( ( y u. { z } ) X. { J } ) |` y ) |
92 |
91
|
fveq2i |
|- ( Xt_ ` ( y X. { J } ) ) = ( Xt_ ` ( ( ( y u. { z } ) X. { J } ) |` y ) ) |
93 |
88 76 92
|
ptrescn |
|- ( ( ( y u. { z } ) e. Fin /\ ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top /\ y C_ ( y u. { z } ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w |` y ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( Xt_ ` ( y X. { J } ) ) ) ) |
94 |
61 85 87 93
|
syl3anc |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w |` y ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( Xt_ ` ( y X. { J } ) ) ) ) |
95 |
81 94
|
eqeltrd |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w |` y ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( Xt_ ` ( y X. { J } ) ) ) ) |
96 |
|
eqid |
|- ( Xt_ ` ( y X. { J } ) ) = ( Xt_ ` ( y X. { J } ) ) |
97 |
96
|
pttoponconst |
|- ( ( y e. Fin /\ J e. ( TopOn ` B ) ) -> ( Xt_ ` ( y X. { J } ) ) e. ( TopOn ` ( B ^m y ) ) ) |
98 |
58 75 97
|
syl2anc |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( Xt_ ` ( y X. { J } ) ) e. ( TopOn ` ( B ^m y ) ) ) |
99 |
|
simp3 |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) |
100 |
|
oveq2 |
|- ( x = ( w |` y ) -> ( G gsum x ) = ( G gsum ( w |` y ) ) ) |
101 |
78 95 98 99 100
|
cnmpt11 |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum ( w |` y ) ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
102 |
64
|
feqmptd |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> w = ( k e. ( y u. { z } ) |-> ( w ` k ) ) ) |
103 |
102
|
reseq1d |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( w |` { z } ) = ( ( k e. ( y u. { z } ) |-> ( w ` k ) ) |` { z } ) ) |
104 |
|
ssun2 |
|- { z } C_ ( y u. { z } ) |
105 |
|
resmpt |
|- ( { z } C_ ( y u. { z } ) -> ( ( k e. ( y u. { z } ) |-> ( w ` k ) ) |` { z } ) = ( k e. { z } |-> ( w ` k ) ) ) |
106 |
104 105
|
ax-mp |
|- ( ( k e. ( y u. { z } ) |-> ( w ` k ) ) |` { z } ) = ( k e. { z } |-> ( w ` k ) ) |
107 |
103 106
|
eqtrdi |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( w |` { z } ) = ( k e. { z } |-> ( w ` k ) ) ) |
108 |
107
|
oveq2d |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum ( w |` { z } ) ) = ( G gsum ( k e. { z } |-> ( w ` k ) ) ) ) |
109 |
|
cmnmnd |
|- ( G e. CMnd -> G e. Mnd ) |
110 |
57 109
|
syl |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> G e. Mnd ) |
111 |
|
vex |
|- z e. _V |
112 |
111
|
a1i |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> z e. _V ) |
113 |
|
vsnid |
|- z e. { z } |
114 |
|
elun2 |
|- ( z e. { z } -> z e. ( y u. { z } ) ) |
115 |
113 114
|
mp1i |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> z e. ( y u. { z } ) ) |
116 |
64 115
|
ffvelrnd |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( w ` z ) e. B ) |
117 |
|
fveq2 |
|- ( k = z -> ( w ` k ) = ( w ` z ) ) |
118 |
2 117
|
gsumsn |
|- ( ( G e. Mnd /\ z e. _V /\ ( w ` z ) e. B ) -> ( G gsum ( k e. { z } |-> ( w ` k ) ) ) = ( w ` z ) ) |
119 |
110 112 116 118
|
syl3anc |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum ( k e. { z } |-> ( w ` k ) ) ) = ( w ` z ) ) |
120 |
108 119
|
eqtrd |
|- ( ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) /\ w e. ( B ^m ( y u. { z } ) ) ) -> ( G gsum ( w |` { z } ) ) = ( w ` z ) ) |
121 |
120
|
mpteq2dva |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum ( w |` { z } ) ) ) = ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) ) |
122 |
80
|
mpteq1d |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) = ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w ` z ) ) ) |
123 |
113 114
|
mp1i |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> z e. ( y u. { z } ) ) |
124 |
88 76
|
ptpjcn |
|- ( ( ( y u. { z } ) e. Fin /\ ( ( y u. { z } ) X. { J } ) : ( y u. { z } ) --> Top /\ z e. ( y u. { z } ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) ) |
125 |
61 85 123 124
|
syl3anc |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. U. ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) ) |
126 |
122 125
|
eqeltrd |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) ) |
127 |
|
fvconst2g |
|- ( ( J e. Top /\ z e. ( y u. { z } ) ) -> ( ( ( y u. { z } ) X. { J } ) ` z ) = J ) |
128 |
83 123 127
|
syl2anc |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( ( y u. { z } ) X. { J } ) ` z ) = J ) |
129 |
128
|
oveq2d |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn ( ( ( y u. { z } ) X. { J } ) ` z ) ) = ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
130 |
126 129
|
eleqtrd |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( w ` z ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
131 |
121 130
|
eqeltrd |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( G gsum ( w |` { z } ) ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
132 |
1 56 74 78 101 131
|
cnmpt1plusg |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( w e. ( B ^m ( y u. { z } ) ) |-> ( ( G gsum ( w |` y ) ) ( +g ` G ) ( G gsum ( w |` { z } ) ) ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
133 |
73 132
|
eqeltrd |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) /\ ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) |
134 |
133
|
3expia |
|- ( ( ( G e. CMnd /\ G e. TopMnd ) /\ ( y e. Fin /\ -. z e. y ) ) -> ( ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) |
135 |
134
|
expcom |
|- ( ( y e. Fin /\ -. z e. y ) -> ( ( G e. CMnd /\ G e. TopMnd ) -> ( ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) ) |
136 |
135
|
a2d |
|- ( ( y e. Fin /\ -. z e. y ) -> ( ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m y ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( y X. { J } ) ) Cn J ) ) -> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m ( y u. { z } ) ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( ( y u. { z } ) X. { J } ) ) Cn J ) ) ) ) |
137 |
11 18 25 32 53 136
|
findcard2s |
|- ( A e. Fin -> ( ( G e. CMnd /\ G e. TopMnd ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) ) |
138 |
137
|
com12 |
|- ( ( G e. CMnd /\ G e. TopMnd ) -> ( A e. Fin -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) ) |
139 |
138
|
3impia |
|- ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) |
140 |
42 82
|
syl |
|- ( G e. TopMnd -> J e. Top ) |
141 |
|
xkopt |
|- ( ( J e. Top /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) ) |
142 |
140 141
|
sylan |
|- ( ( G e. TopMnd /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) ) |
143 |
142
|
3adant1 |
|- ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( J ^ko ~P A ) = ( Xt_ ` ( A X. { J } ) ) ) |
144 |
143
|
oveq1d |
|- ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( ( J ^ko ~P A ) Cn J ) = ( ( Xt_ ` ( A X. { J } ) ) Cn J ) ) |
145 |
139 144
|
eleqtrrd |
|- ( ( G e. CMnd /\ G e. TopMnd /\ A e. Fin ) -> ( x e. ( B ^m A ) |-> ( G gsum x ) ) e. ( ( J ^ko ~P A ) Cn J ) ) |