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 )