Metamath Proof Explorer

Theorem tsmsxplem2

Description: Lemma for tsmsxp . (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmsxp.b 
|- B = ( Base ` G )
tsmsxp.g 
|- ( ph -> G e. CMnd )
tsmsxp.2 
|- ( ph -> G e. TopGrp )
tsmsxp.a 
|- ( ph -> A e. V )
tsmsxp.c 
|- ( ph -> C e. W )
tsmsxp.f 
|- ( ph -> F : ( A X. C ) --> B )
tsmsxp.h 
|- ( ph -> H : A --> B )
tsmsxp.1 
|- ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
tsmsxp.j 
|- J = ( TopOpen ` G )
tsmsxp.z 
|- .0. = ( 0g ` G )
tsmsxp.p 
|- .+ = ( +g ` G )
tsmsxp.m 
|- .- = ( -g ` G )
tsmsxp.l 
|- ( ph -> L e. J )
tsmsxp.3 
|- ( ph -> .0. e. L )
tsmsxp.k 
|- ( ph -> K e. ( ~P A i^i Fin ) )
tsmsxp.4 
|- ( ph -> A. c e. S A. d e. T ( c .+ d ) e. U )
tsmsxp.n 
|- ( ph -> N e. ( ~P C i^i Fin ) )
tsmsxp.s 
|- ( ph -> D C_ ( K X. N ) )
tsmsxp.x 
|- ( ph -> A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L )
tsmsxp.5 
|- ( ph -> ( G gsum ( F |` ( K X. N ) ) ) e. S )
tsmsxp.6 
|- ( ph -> A. g e. ( L ^m K ) ( G gsum g ) e. T )
Assertion tsmsxplem2 
|- ( ph -> ( G gsum ( H |` K ) ) e. U )

Proof

Step Hyp Ref Expression
1 tsmsxp.b 
 |-  B = ( Base ` G )
2 tsmsxp.g 
 |-  ( ph -> G e. CMnd )
3 tsmsxp.2 
 |-  ( ph -> G e. TopGrp )
4 tsmsxp.a 
 |-  ( ph -> A e. V )
5 tsmsxp.c 
 |-  ( ph -> C e. W )
6 tsmsxp.f 
 |-  ( ph -> F : ( A X. C ) --> B )
7 tsmsxp.h 
 |-  ( ph -> H : A --> B )
8 tsmsxp.1 
 |-  ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
9 tsmsxp.j 
 |-  J = ( TopOpen ` G )
10 tsmsxp.z 
 |-  .0. = ( 0g ` G )
11 tsmsxp.p 
 |-  .+ = ( +g ` G )
12 tsmsxp.m 
 |-  .- = ( -g ` G )
13 tsmsxp.l 
 |-  ( ph -> L e. J )
14 tsmsxp.3 
 |-  ( ph -> .0. e. L )
15 tsmsxp.k 
 |-  ( ph -> K e. ( ~P A i^i Fin ) )
16 tsmsxp.4 
 |-  ( ph -> A. c e. S A. d e. T ( c .+ d ) e. U )
17 tsmsxp.n 
 |-  ( ph -> N e. ( ~P C i^i Fin ) )
18 tsmsxp.s 
 |-  ( ph -> D C_ ( K X. N ) )
19 tsmsxp.x 
 |-  ( ph -> A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L )
20 tsmsxp.5 
 |-  ( ph -> ( G gsum ( F |` ( K X. N ) ) ) e. S )
21 tsmsxp.6 
 |-  ( ph -> A. g e. ( L ^m K ) ( G gsum g ) e. T )
22 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
23 3 22 syl 
 |-  ( ph -> G e. Grp )
24 isabl 
 |-  ( G e. Abel <-> ( G e. Grp /\ G e. CMnd ) )
25 23 2 24 sylanbrc 
 |-  ( ph -> G e. Abel )
26 15 elin2d 
 |-  ( ph -> K e. Fin )
27 17 elin2d 
 |-  ( ph -> N e. Fin )
28 xpfi 
 |-  ( ( K e. Fin /\ N e. Fin ) -> ( K X. N ) e. Fin )
29 26 27 28 syl2anc 
 |-  ( ph -> ( K X. N ) e. Fin )
30 elfpw 
 |-  ( K e. ( ~P A i^i Fin ) <-> ( K C_ A /\ K e. Fin ) )
31 30 simplbi 
 |-  ( K e. ( ~P A i^i Fin ) -> K C_ A )
32 15 31 syl 
 |-  ( ph -> K C_ A )
33 elfpw 
 |-  ( N e. ( ~P C i^i Fin ) <-> ( N C_ C /\ N e. Fin ) )
34 33 simplbi 
 |-  ( N e. ( ~P C i^i Fin ) -> N C_ C )
35 17 34 syl 
 |-  ( ph -> N C_ C )
36 xpss12 
 |-  ( ( K C_ A /\ N C_ C ) -> ( K X. N ) C_ ( A X. C ) )
37 32 35 36 syl2anc 
 |-  ( ph -> ( K X. N ) C_ ( A X. C ) )
38 6 37 fssresd 
 |-  ( ph -> ( F |` ( K X. N ) ) : ( K X. N ) --> B )
39 38 29 14 fdmfifsupp 
 |-  ( ph -> ( F |` ( K X. N ) ) finSupp .0. )
40 1 10 2 29 38 39 gsumcl 
 |-  ( ph -> ( G gsum ( F |` ( K X. N ) ) ) e. B )
41 7 32 fssresd 
 |-  ( ph -> ( H |` K ) : K --> B )
42 41 26 14 fdmfifsupp 
 |-  ( ph -> ( H |` K ) finSupp .0. )
43 1 10 2 15 41 42 gsumcl 
 |-  ( ph -> ( G gsum ( H |` K ) ) e. B )
44 1 11 12 ablpncan3 
 |-  ( ( G e. Abel /\ ( ( G gsum ( F |` ( K X. N ) ) ) e. B /\ ( G gsum ( H |` K ) ) e. B ) ) -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) = ( G gsum ( H |` K ) ) )
45 25 40 43 44 syl12anc 
 |-  ( ph -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) = ( G gsum ( H |` K ) ) )
46 2 adantr 
 |-  ( ( ph /\ y e. K ) -> G e. CMnd )
47 snfi 
 |-  { y } e. Fin
48 27 adantr 
 |-  ( ( ph /\ y e. K ) -> N e. Fin )
49 xpfi 
 |-  ( ( { y } e. Fin /\ N e. Fin ) -> ( { y } X. N ) e. Fin )
50 47 48 49 sylancr 
 |-  ( ( ph /\ y e. K ) -> ( { y } X. N ) e. Fin )
51 6 adantr 
 |-  ( ( ph /\ y e. K ) -> F : ( A X. C ) --> B )
52 32 sselda 
 |-  ( ( ph /\ y e. K ) -> y e. A )
53 52 snssd 
 |-  ( ( ph /\ y e. K ) -> { y } C_ A )
54 35 adantr 
 |-  ( ( ph /\ y e. K ) -> N C_ C )
55 xpss12 
 |-  ( ( { y } C_ A /\ N C_ C ) -> ( { y } X. N ) C_ ( A X. C ) )
56 53 54 55 syl2anc 
 |-  ( ( ph /\ y e. K ) -> ( { y } X. N ) C_ ( A X. C ) )
57 51 56 fssresd 
 |-  ( ( ph /\ y e. K ) -> ( F |` ( { y } X. N ) ) : ( { y } X. N ) --> B )
58 10 fvexi 
 |-  .0. e. _V
59 58 a1i 
 |-  ( ( ph /\ y e. K ) -> .0. e. _V )
60 57 50 59 fdmfifsupp 
 |-  ( ( ph /\ y e. K ) -> ( F |` ( { y } X. N ) ) finSupp .0. )
61 1 10 46 50 57 60 gsumcl 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) e. B )
62 61 fmpttd 
 |-  ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) : K --> B )
63 eqid 
 |-  ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) = ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) )
64 ovexd 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) e. _V )
65 63 26 64 14 fsuppmptdm 
 |-  ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) finSupp .0. )
66 1 10 12 25 15 41 62 42 65 gsumsub 
 |-  ( ph -> ( G gsum ( ( H |` K ) oF .- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( ( G gsum ( H |` K ) ) .- ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) )
67 fvexd 
 |-  ( ( ph /\ y e. K ) -> ( H ` y ) e. _V )
68 7 32 feqresmpt 
 |-  ( ph -> ( H |` K ) = ( y e. K |-> ( H ` y ) ) )
69 eqidd 
 |-  ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) = ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) )
70 15 67 64 68 69 offval2 
 |-  ( ph -> ( ( H |` K ) oF .- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) = ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) )
71 70 oveq2d 
 |-  ( ph -> ( G gsum ( ( H |` K ) oF .- ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) )
72 cmnmnd 
 |-  ( G e. CMnd -> G e. Mnd )
73 46 72 syl 
 |-  ( ( ph /\ y e. K ) -> G e. Mnd )
74 simpr 
 |-  ( ( ph /\ y e. K ) -> y e. K )
75 51 adantr 
 |-  ( ( ( ph /\ y e. K ) /\ z e. N ) -> F : ( A X. C ) --> B )
76 52 adantr 
 |-  ( ( ( ph /\ y e. K ) /\ z e. N ) -> y e. A )
77 54 sselda 
 |-  ( ( ( ph /\ y e. K ) /\ z e. N ) -> z e. C )
78 75 76 77 fovrnd 
 |-  ( ( ( ph /\ y e. K ) /\ z e. N ) -> ( y F z ) e. B )
79 78 fmpttd 
 |-  ( ( ph /\ y e. K ) -> ( z e. N |-> ( y F z ) ) : N --> B )
80 eqid 
 |-  ( z e. N |-> ( y F z ) ) = ( z e. N |-> ( y F z ) )
81 ovexd 
 |-  ( ( ( ph /\ y e. K ) /\ z e. N ) -> ( y F z ) e. _V )
82 80 48 81 59 fsuppmptdm 
 |-  ( ( ph /\ y e. K ) -> ( z e. N |-> ( y F z ) ) finSupp .0. )
83 1 10 46 48 79 82 gsumcl 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( z e. N |-> ( y F z ) ) ) e. B )
84 velsn 
 |-  ( w e. { y } <-> w = y )
85 ovres 
 |-  ( ( w e. { y } /\ z e. N ) -> ( w ( F |` ( { y } X. N ) ) z ) = ( w F z ) )
86 84 85 sylanbr 
 |-  ( ( w = y /\ z e. N ) -> ( w ( F |` ( { y } X. N ) ) z ) = ( w F z ) )
87 oveq1 
 |-  ( w = y -> ( w F z ) = ( y F z ) )
88 87 adantr 
 |-  ( ( w = y /\ z e. N ) -> ( w F z ) = ( y F z ) )
89 86 88 eqtrd 
 |-  ( ( w = y /\ z e. N ) -> ( w ( F |` ( { y } X. N ) ) z ) = ( y F z ) )
90 89 mpteq2dva 
 |-  ( w = y -> ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) = ( z e. N |-> ( y F z ) ) )
91 90 oveq2d 
 |-  ( w = y -> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) )
92 1 91 gsumsn 
 |-  ( ( G e. Mnd /\ y e. K /\ ( G gsum ( z e. N |-> ( y F z ) ) ) e. B ) -> ( G gsum ( w e. { y } |-> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) )
93 73 74 83 92 syl3anc 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( w e. { y } |-> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) )
94 47 a1i 
 |-  ( ( ph /\ y e. K ) -> { y } e. Fin )
95 1 10 46 94 48 57 60 gsumxp 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) = ( G gsum ( w e. { y } |-> ( G gsum ( z e. N |-> ( w ( F |` ( { y } X. N ) ) z ) ) ) ) ) )
96 ovres 
 |-  ( ( y e. K /\ z e. N ) -> ( y ( F |` ( K X. N ) ) z ) = ( y F z ) )
97 96 adantll 
 |-  ( ( ( ph /\ y e. K ) /\ z e. N ) -> ( y ( F |` ( K X. N ) ) z ) = ( y F z ) )
98 97 mpteq2dva 
 |-  ( ( ph /\ y e. K ) -> ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) = ( z e. N |-> ( y F z ) ) )
99 98 oveq2d 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) = ( G gsum ( z e. N |-> ( y F z ) ) ) )
100 93 95 99 3eqtr4d 
 |-  ( ( ph /\ y e. K ) -> ( G gsum ( F |` ( { y } X. N ) ) ) = ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) )
101 100 mpteq2dva 
 |-  ( ph -> ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) = ( y e. K |-> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) )
102 101 oveq2d 
 |-  ( ph -> ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) = ( G gsum ( y e. K |-> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) ) )
103 1 10 2 26 27 38 39 gsumxp 
 |-  ( ph -> ( G gsum ( F |` ( K X. N ) ) ) = ( G gsum ( y e. K |-> ( G gsum ( z e. N |-> ( y ( F |` ( K X. N ) ) z ) ) ) ) ) )
104 102 103 eqtr4d 
 |-  ( ph -> ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) = ( G gsum ( F |` ( K X. N ) ) ) )
105 104 oveq2d 
 |-  ( ph -> ( ( G gsum ( H |` K ) ) .- ( G gsum ( y e. K |-> ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) )
106 66 71 105 3eqtr3d 
 |-  ( ph -> ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) )
107 oveq2 
 |-  ( g = ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) -> ( G gsum g ) = ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) )
108 107 eleq1d 
 |-  ( g = ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) -> ( ( G gsum g ) e. T <-> ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) e. T ) )
109 fveq2 
 |-  ( x = y -> ( H ` x ) = ( H ` y ) )
110 sneq 
 |-  ( x = y -> { x } = { y } )
111 110 xpeq1d 
 |-  ( x = y -> ( { x } X. N ) = ( { y } X. N ) )
112 111 reseq2d 
 |-  ( x = y -> ( F |` ( { x } X. N ) ) = ( F |` ( { y } X. N ) ) )
113 112 oveq2d 
 |-  ( x = y -> ( G gsum ( F |` ( { x } X. N ) ) ) = ( G gsum ( F |` ( { y } X. N ) ) ) )
114 109 113 oveq12d 
 |-  ( x = y -> ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) = ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) )
115 114 eleq1d 
 |-  ( x = y -> ( ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L <-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) e. L ) )
116 115 rspccva 
 |-  ( ( A. x e. K ( ( H ` x ) .- ( G gsum ( F |` ( { x } X. N ) ) ) ) e. L /\ y e. K ) -> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) e. L )
117 19 116 sylan 
 |-  ( ( ph /\ y e. K ) -> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) e. L )
118 117 fmpttd 
 |-  ( ph -> ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) : K --> L )
119 13 15 elmapd 
 |-  ( ph -> ( ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) e. ( L ^m K ) <-> ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) : K --> L ) )
120 118 119 mpbird 
 |-  ( ph -> ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) e. ( L ^m K ) )
121 108 21 120 rspcdva 
 |-  ( ph -> ( G gsum ( y e. K |-> ( ( H ` y ) .- ( G gsum ( F |` ( { y } X. N ) ) ) ) ) ) e. T )
122 106 121 eqeltrrd 
 |-  ( ph -> ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) e. T )
123 oveq1 
 |-  ( c = ( G gsum ( F |` ( K X. N ) ) ) -> ( c .+ d ) = ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) )
124 123 eleq1d 
 |-  ( c = ( G gsum ( F |` ( K X. N ) ) ) -> ( ( c .+ d ) e. U <-> ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) e. U ) )
125 oveq2 
 |-  ( d = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) = ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) )
126 125 eleq1d 
 |-  ( d = ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) -> ( ( ( G gsum ( F |` ( K X. N ) ) ) .+ d ) e. U <-> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) e. U ) )
127 124 126 rspc2va 
 |-  ( ( ( ( G gsum ( F |` ( K X. N ) ) ) e. S /\ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) e. T ) /\ A. c e. S A. d e. T ( c .+ d ) e. U ) -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) e. U )
128 20 122 16 127 syl21anc 
 |-  ( ph -> ( ( G gsum ( F |` ( K X. N ) ) ) .+ ( ( G gsum ( H |` K ) ) .- ( G gsum ( F |` ( K X. N ) ) ) ) ) e. U )
129 45 128 eqeltrrd 
 |-  ( ph -> ( G gsum ( H |` K ) ) e. U )