Metamath Proof Explorer

Theorem gsumle

Description: A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018)

Ref Expression
Hypotheses gsumle.b 
|- B = ( Base ` M )
gsumle.l 
|- .<_ = ( le ` M )
gsumle.m 
|- ( ph -> M e. oMnd )
gsumle.n 
|- ( ph -> M e. CMnd )
gsumle.a 
|- ( ph -> A e. Fin )
gsumle.f 
|- ( ph -> F : A --> B )
gsumle.g 
|- ( ph -> G : A --> B )
gsumle.c 
|- ( ph -> F oR .<_ G )
Assertion gsumle 
|- ( ph -> ( M gsum F ) .<_ ( M gsum G ) )

Proof

Step Hyp Ref Expression
1 gsumle.b 
 |-  B = ( Base ` M )
2 gsumle.l 
 |-  .<_ = ( le ` M )
3 gsumle.m 
 |-  ( ph -> M e. oMnd )
4 gsumle.n 
 |-  ( ph -> M e. CMnd )
5 gsumle.a 
 |-  ( ph -> A e. Fin )
6 gsumle.f 
 |-  ( ph -> F : A --> B )
7 gsumle.g 
 |-  ( ph -> G : A --> B )
8 gsumle.c 
 |-  ( ph -> F oR .<_ G )
9 ssid 
 |-  A C_ A
10 sseq1 
 |-  ( a = (/) -> ( a C_ A <-> (/) C_ A ) )
11 10 anbi2d 
 |-  ( a = (/) -> ( ( ph /\ a C_ A ) <-> ( ph /\ (/) C_ A ) ) )
12 reseq2 
 |-  ( a = (/) -> ( F |` a ) = ( F |` (/) ) )
13 12 oveq2d 
 |-  ( a = (/) -> ( M gsum ( F |` a ) ) = ( M gsum ( F |` (/) ) ) )
14 reseq2 
 |-  ( a = (/) -> ( G |` a ) = ( G |` (/) ) )
15 14 oveq2d 
 |-  ( a = (/) -> ( M gsum ( G |` a ) ) = ( M gsum ( G |` (/) ) ) )
16 13 15 breq12d 
 |-  ( a = (/) -> ( ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) <-> ( M gsum ( F |` (/) ) ) .<_ ( M gsum ( G |` (/) ) ) ) )
17 11 16 imbi12d 
 |-  ( a = (/) -> ( ( ( ph /\ a C_ A ) -> ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) ) <-> ( ( ph /\ (/) C_ A ) -> ( M gsum ( F |` (/) ) ) .<_ ( M gsum ( G |` (/) ) ) ) ) )
18 sseq1 
 |-  ( a = e -> ( a C_ A <-> e C_ A ) )
19 18 anbi2d 
 |-  ( a = e -> ( ( ph /\ a C_ A ) <-> ( ph /\ e C_ A ) ) )
20 reseq2 
 |-  ( a = e -> ( F |` a ) = ( F |` e ) )
21 20 oveq2d 
 |-  ( a = e -> ( M gsum ( F |` a ) ) = ( M gsum ( F |` e ) ) )
22 reseq2 
 |-  ( a = e -> ( G |` a ) = ( G |` e ) )
23 22 oveq2d 
 |-  ( a = e -> ( M gsum ( G |` a ) ) = ( M gsum ( G |` e ) ) )
24 21 23 breq12d 
 |-  ( a = e -> ( ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) <-> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) )
25 19 24 imbi12d 
 |-  ( a = e -> ( ( ( ph /\ a C_ A ) -> ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) ) <-> ( ( ph /\ e C_ A ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) ) )
26 sseq1 
 |-  ( a = ( e u. { y } ) -> ( a C_ A <-> ( e u. { y } ) C_ A ) )
27 26 anbi2d 
 |-  ( a = ( e u. { y } ) -> ( ( ph /\ a C_ A ) <-> ( ph /\ ( e u. { y } ) C_ A ) ) )
28 reseq2 
 |-  ( a = ( e u. { y } ) -> ( F |` a ) = ( F |` ( e u. { y } ) ) )
29 28 oveq2d 
 |-  ( a = ( e u. { y } ) -> ( M gsum ( F |` a ) ) = ( M gsum ( F |` ( e u. { y } ) ) ) )
30 reseq2 
 |-  ( a = ( e u. { y } ) -> ( G |` a ) = ( G |` ( e u. { y } ) ) )
31 30 oveq2d 
 |-  ( a = ( e u. { y } ) -> ( M gsum ( G |` a ) ) = ( M gsum ( G |` ( e u. { y } ) ) ) )
32 29 31 breq12d 
 |-  ( a = ( e u. { y } ) -> ( ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) <-> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) ) )
33 27 32 imbi12d 
 |-  ( a = ( e u. { y } ) -> ( ( ( ph /\ a C_ A ) -> ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) ) <-> ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) ) ) )
34 sseq1 
 |-  ( a = A -> ( a C_ A <-> A C_ A ) )
35 34 anbi2d 
 |-  ( a = A -> ( ( ph /\ a C_ A ) <-> ( ph /\ A C_ A ) ) )
36 reseq2 
 |-  ( a = A -> ( F |` a ) = ( F |` A ) )
37 36 oveq2d 
 |-  ( a = A -> ( M gsum ( F |` a ) ) = ( M gsum ( F |` A ) ) )
38 reseq2 
 |-  ( a = A -> ( G |` a ) = ( G |` A ) )
39 38 oveq2d 
 |-  ( a = A -> ( M gsum ( G |` a ) ) = ( M gsum ( G |` A ) ) )
40 37 39 breq12d 
 |-  ( a = A -> ( ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) <-> ( M gsum ( F |` A ) ) .<_ ( M gsum ( G |` A ) ) ) )
41 35 40 imbi12d 
 |-  ( a = A -> ( ( ( ph /\ a C_ A ) -> ( M gsum ( F |` a ) ) .<_ ( M gsum ( G |` a ) ) ) <-> ( ( ph /\ A C_ A ) -> ( M gsum ( F |` A ) ) .<_ ( M gsum ( G |` A ) ) ) ) )
42 omndtos 
 |-  ( M e. oMnd -> M e. Toset )
43 tospos 
 |-  ( M e. Toset -> M e. Poset )
44 3 42 43 3syl 
 |-  ( ph -> M e. Poset )
45 res0 
 |-  ( F |` (/) ) = (/)
46 45 oveq2i 
 |-  ( M gsum ( F |` (/) ) ) = ( M gsum (/) )
47 eqid 
 |-  ( 0g ` M ) = ( 0g ` M )
48 47 gsum0 
 |-  ( M gsum (/) ) = ( 0g ` M )
49 46 48 eqtri 
 |-  ( M gsum ( F |` (/) ) ) = ( 0g ` M )
50 omndmnd 
 |-  ( M e. oMnd -> M e. Mnd )
51 1 47 mndidcl 
 |-  ( M e. Mnd -> ( 0g ` M ) e. B )
52 3 50 51 3syl 
 |-  ( ph -> ( 0g ` M ) e. B )
53 49 52 eqeltrid 
 |-  ( ph -> ( M gsum ( F |` (/) ) ) e. B )
54 1 2 posref 
 |-  ( ( M e. Poset /\ ( M gsum ( F |` (/) ) ) e. B ) -> ( M gsum ( F |` (/) ) ) .<_ ( M gsum ( F |` (/) ) ) )
55 44 53 54 syl2anc 
 |-  ( ph -> ( M gsum ( F |` (/) ) ) .<_ ( M gsum ( F |` (/) ) ) )
56 res0 
 |-  ( G |` (/) ) = (/)
57 45 56 eqtr4i 
 |-  ( F |` (/) ) = ( G |` (/) )
58 57 oveq2i 
 |-  ( M gsum ( F |` (/) ) ) = ( M gsum ( G |` (/) ) )
59 55 58 breqtrdi 
 |-  ( ph -> ( M gsum ( F |` (/) ) ) .<_ ( M gsum ( G |` (/) ) ) )
60 59 adantr 
 |-  ( ( ph /\ (/) C_ A ) -> ( M gsum ( F |` (/) ) ) .<_ ( M gsum ( G |` (/) ) ) )
61 ssun1 
 |-  e C_ ( e u. { y } )
62 sstr2 
 |-  ( e C_ ( e u. { y } ) -> ( ( e u. { y } ) C_ A -> e C_ A ) )
63 61 62 ax-mp 
 |-  ( ( e u. { y } ) C_ A -> e C_ A )
64 63 anim2i 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ph /\ e C_ A ) )
65 64 imim1i 
 |-  ( ( ( ph /\ e C_ A ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) )
66 simplr 
 |-  ( ( ( ( e e. Fin /\ -. y e. e ) /\ ( ph /\ ( e u. { y } ) C_ A ) ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( ph /\ ( e u. { y } ) C_ A ) )
67 simpllr 
 |-  ( ( ( ( e e. Fin /\ -. y e. e ) /\ ( ph /\ ( e u. { y } ) C_ A ) ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> -. y e. e )
68 simpr 
 |-  ( ( ( ( e e. Fin /\ -. y e. e ) /\ ( ph /\ ( e u. { y } ) C_ A ) ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) )
69 eqid 
 |-  ( +g ` M ) = ( +g ` M )
70 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> M e. oMnd )
71 7 ad2antrr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> G : A --> B )
72 simplr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( e u. { y } ) C_ A )
73 ssun2 
 |-  { y } C_ ( e u. { y } )
74 vex 
 |-  y e. _V
75 74 snss 
 |-  ( y e. ( e u. { y } ) <-> { y } C_ ( e u. { y } ) )
76 73 75 mpbir 
 |-  y e. ( e u. { y } )
77 76 a1i 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> y e. ( e u. { y } ) )
78 72 77 sseldd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> y e. A )
79 71 78 ffvelcdmd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( G ` y ) e. B )
80 79 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( G ` y ) e. B )
81 4 ad2antrr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> M e. CMnd )
82 vex 
 |-  e e. _V
83 82 a1i 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> e e. _V )
84 6 ad2antrr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> F : A --> B )
85 61 72 sstrid 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> e C_ A )
86 84 85 fssresd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( F |` e ) : e --> B )
87 5 ad2antrr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> A e. Fin )
88 fvexd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( 0g ` M ) e. _V )
89 84 87 88 fdmfifsupp 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> F finSupp ( 0g ` M ) )
90 89 88 fsuppres 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( F |` e ) finSupp ( 0g ` M ) )
91 1 47 81 83 86 90 gsumcl 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( F |` e ) ) e. B )
92 91 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( F |` e ) ) e. B )
93 84 78 ffvelcdmd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( F ` y ) e. B )
94 93 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( F ` y ) e. B )
95 71 85 fssresd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( G |` e ) : e --> B )
96 ssfi 
 |-  ( ( A e. Fin /\ e C_ A ) -> e e. Fin )
97 87 85 96 syl2anc 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> e e. Fin )
98 95 97 88 fdmfifsupp 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( G |` e ) finSupp ( 0g ` M ) )
99 1 47 81 83 95 98 gsumcl 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( G |` e ) ) e. B )
100 99 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( G |` e ) ) e. B )
101 simpr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) )
102 simpll 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ph )
103 8 ad2antrr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> F oR .<_ G )
104 6 ffnd 
 |-  ( ph -> F Fn A )
105 7 ffnd 
 |-  ( ph -> G Fn A )
106 inidm 
 |-  ( A i^i A ) = A
107 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( F ` y ) )
108 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( G ` y ) = ( G ` y ) )
109 104 105 5 5 106 107 108 ofrval 
 |-  ( ( ph /\ F oR .<_ G /\ y e. A ) -> ( F ` y ) .<_ ( G ` y ) )
110 102 103 78 109 syl3anc 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( F ` y ) .<_ ( G ` y ) )
111 110 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( F ` y ) .<_ ( G ` y ) )
112 81 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> M e. CMnd )
113 1 2 69 70 80 92 94 100 101 111 112 omndadd2d 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( ( M gsum ( F |` e ) ) ( +g ` M ) ( F ` y ) ) .<_ ( ( M gsum ( G |` e ) ) ( +g ` M ) ( G ` y ) ) )
114 97 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> e e. Fin )
115 6 ad2antrr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ z e. e ) -> F : A --> B )
116 simplr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ z e. e ) -> ( e u. { y } ) C_ A )
117 elun1 
 |-  ( z e. e -> z e. ( e u. { y } ) )
118 117 adantl 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ z e. e ) -> z e. ( e u. { y } ) )
119 116 118 sseldd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ z e. e ) -> z e. A )
120 115 119 ffvelcdmd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ z e. e ) -> ( F ` z ) e. B )
121 120 ex 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( z e. e -> ( F ` z ) e. B ) )
122 121 ad2antrr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( z e. e -> ( F ` z ) e. B ) )
123 122 imp 
 |-  ( ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) /\ z e. e ) -> ( F ` z ) e. B )
124 74 a1i 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> y e. _V )
125 simplr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> -. y e. e )
126 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
127 1 69 112 114 123 124 125 94 126 gsumunsn 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( z e. ( e u. { y } ) |-> ( F ` z ) ) ) = ( ( M gsum ( z e. e |-> ( F ` z ) ) ) ( +g ` M ) ( F ` y ) ) )
128 84 72 feqresmpt 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( F |` ( e u. { y } ) ) = ( z e. ( e u. { y } ) |-> ( F ` z ) ) )
129 128 oveq2d 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( F |` ( e u. { y } ) ) ) = ( M gsum ( z e. ( e u. { y } ) |-> ( F ` z ) ) ) )
130 84 85 feqresmpt 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( F |` e ) = ( z e. e |-> ( F ` z ) ) )
131 130 oveq2d 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( F |` e ) ) = ( M gsum ( z e. e |-> ( F ` z ) ) ) )
132 131 oveq1d 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( ( M gsum ( F |` e ) ) ( +g ` M ) ( F ` y ) ) = ( ( M gsum ( z e. e |-> ( F ` z ) ) ) ( +g ` M ) ( F ` y ) ) )
133 129 132 eqeq12d 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( ( M gsum ( F |` ( e u. { y } ) ) ) = ( ( M gsum ( F |` e ) ) ( +g ` M ) ( F ` y ) ) <-> ( M gsum ( z e. ( e u. { y } ) |-> ( F ` z ) ) ) = ( ( M gsum ( z e. e |-> ( F ` z ) ) ) ( +g ` M ) ( F ` y ) ) ) )
134 133 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( ( M gsum ( F |` ( e u. { y } ) ) ) = ( ( M gsum ( F |` e ) ) ( +g ` M ) ( F ` y ) ) <-> ( M gsum ( z e. ( e u. { y } ) |-> ( F ` z ) ) ) = ( ( M gsum ( z e. e |-> ( F ` z ) ) ) ( +g ` M ) ( F ` y ) ) ) )
135 127 134 mpbird 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( F |` ( e u. { y } ) ) ) = ( ( M gsum ( F |` e ) ) ( +g ` M ) ( F ` y ) ) )
136 7 adantr 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> G : A --> B )
137 136 ad2antrr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ z e. e ) -> G : A --> B )
138 119 adantlr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ z e. e ) -> z e. A )
139 137 138 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ z e. e ) -> ( G ` z ) e. B )
140 74 a1i 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> y e. _V )
141 simpr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> -. y e. e )
142 fveq2 
 |-  ( z = y -> ( G ` z ) = ( G ` y ) )
143 1 69 81 97 139 140 141 79 142 gsumunsn 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( z e. ( e u. { y } ) |-> ( G ` z ) ) ) = ( ( M gsum ( z e. e |-> ( G ` z ) ) ) ( +g ` M ) ( G ` y ) ) )
144 simpr 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( e u. { y } ) C_ A )
145 136 144 feqresmpt 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( G |` ( e u. { y } ) ) = ( z e. ( e u. { y } ) |-> ( G ` z ) ) )
146 145 oveq2d 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( G |` ( e u. { y } ) ) ) = ( M gsum ( z e. ( e u. { y } ) |-> ( G ` z ) ) ) )
147 resabs1 
 |-  ( e C_ ( e u. { y } ) -> ( ( G |` ( e u. { y } ) ) |` e ) = ( G |` e ) )
148 61 147 mp1i 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( G |` ( e u. { y } ) ) |` e ) = ( G |` e ) )
149 63 adantl 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> e C_ A )
150 136 149 feqresmpt 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( G |` e ) = ( z e. e |-> ( G ` z ) ) )
151 148 150 eqtrd 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( G |` ( e u. { y } ) ) |` e ) = ( z e. e |-> ( G ` z ) ) )
152 151 oveq2d 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) = ( M gsum ( z e. e |-> ( G ` z ) ) ) )
153 resabs1 
 |-  ( { y } C_ ( e u. { y } ) -> ( ( G |` ( e u. { y } ) ) |` { y } ) = ( G |` { y } ) )
154 73 153 mp1i 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( G |` ( e u. { y } ) ) |` { y } ) = ( G |` { y } ) )
155 73 144 sstrid 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> { y } C_ A )
156 136 155 feqresmpt 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( G |` { y } ) = ( z e. { y } |-> ( G ` z ) ) )
157 154 156 eqtrd 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( G |` ( e u. { y } ) ) |` { y } ) = ( z e. { y } |-> ( G ` z ) ) )
158 157 oveq2d 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) = ( M gsum ( z e. { y } |-> ( G ` z ) ) ) )
159 3 50 syl 
 |-  ( ph -> M e. Mnd )
160 159 adantr 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> M e. Mnd )
161 74 a1i 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> y e. _V )
162 76 a1i 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> y e. ( e u. { y } ) )
163 144 162 sseldd 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> y e. A )
164 136 163 ffvelcdmd 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( G ` y ) e. B )
165 142 adantl 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ z = y ) -> ( G ` z ) = ( G ` y ) )
166 1 160 161 164 165 gsumsnd 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( z e. { y } |-> ( G ` z ) ) ) = ( G ` y ) )
167 158 166 eqtrd 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) = ( G ` y ) )
168 152 167 oveq12d 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) ( +g ` M ) ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) ) = ( ( M gsum ( z e. e |-> ( G ` z ) ) ) ( +g ` M ) ( G ` y ) ) )
169 146 168 eqeq12d 
 |-  ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( M gsum ( G |` ( e u. { y } ) ) ) = ( ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) ( +g ` M ) ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) ) <-> ( M gsum ( z e. ( e u. { y } ) |-> ( G ` z ) ) ) = ( ( M gsum ( z e. e |-> ( G ` z ) ) ) ( +g ` M ) ( G ` y ) ) ) )
170 169 adantr 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( ( M gsum ( G |` ( e u. { y } ) ) ) = ( ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) ( +g ` M ) ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) ) <-> ( M gsum ( z e. ( e u. { y } ) |-> ( G ` z ) ) ) = ( ( M gsum ( z e. e |-> ( G ` z ) ) ) ( +g ` M ) ( G ` y ) ) ) )
171 143 170 mpbird 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( G |` ( e u. { y } ) ) ) = ( ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) ( +g ` M ) ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) ) )
172 61 147 ax-mp 
 |-  ( ( G |` ( e u. { y } ) ) |` e ) = ( G |` e )
173 172 oveq2i 
 |-  ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) = ( M gsum ( G |` e ) )
174 73 153 ax-mp 
 |-  ( ( G |` ( e u. { y } ) ) |` { y } ) = ( G |` { y } )
175 174 oveq2i 
 |-  ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) = ( M gsum ( G |` { y } ) )
176 173 175 oveq12i 
 |-  ( ( M gsum ( ( G |` ( e u. { y } ) ) |` e ) ) ( +g ` M ) ( M gsum ( ( G |` ( e u. { y } ) ) |` { y } ) ) ) = ( ( M gsum ( G |` e ) ) ( +g ` M ) ( M gsum ( G |` { y } ) ) )
177 171 176 eqtrdi 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( G |` ( e u. { y } ) ) ) = ( ( M gsum ( G |` e ) ) ( +g ` M ) ( M gsum ( G |` { y } ) ) ) )
178 73 72 sstrid 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> { y } C_ A )
179 71 178 feqresmpt 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( G |` { y } ) = ( x e. { y } |-> ( G ` x ) ) )
180 179 oveq2d 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( G |` { y } ) ) = ( M gsum ( x e. { y } |-> ( G ` x ) ) ) )
181 cmnmnd 
 |-  ( M e. CMnd -> M e. Mnd )
182 81 181 syl 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> M e. Mnd )
183 fveq2 
 |-  ( x = y -> ( G ` x ) = ( G ` y ) )
184 1 183 gsumsn 
 |-  ( ( M e. Mnd /\ y e. _V /\ ( G ` y ) e. B ) -> ( M gsum ( x e. { y } |-> ( G ` x ) ) ) = ( G ` y ) )
185 182 140 79 184 syl3anc 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( x e. { y } |-> ( G ` x ) ) ) = ( G ` y ) )
186 180 185 eqtrd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( G |` { y } ) ) = ( G ` y ) )
187 186 oveq2d 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( ( M gsum ( G |` e ) ) ( +g ` M ) ( M gsum ( G |` { y } ) ) ) = ( ( M gsum ( G |` e ) ) ( +g ` M ) ( G ` y ) ) )
188 177 187 eqtrd 
 |-  ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) -> ( M gsum ( G |` ( e u. { y } ) ) ) = ( ( M gsum ( G |` e ) ) ( +g ` M ) ( G ` y ) ) )
189 188 adantr 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( G |` ( e u. { y } ) ) ) = ( ( M gsum ( G |` e ) ) ( +g ` M ) ( G ` y ) ) )
190 113 135 189 3brtr4d 
 |-  ( ( ( ( ph /\ ( e u. { y } ) C_ A ) /\ -. y e. e ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) )
191 66 67 68 190 syl21anc 
 |-  ( ( ( ( e e. Fin /\ -. y e. e ) /\ ( ph /\ ( e u. { y } ) C_ A ) ) /\ ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) )
192 191 exp31 
 |-  ( ( e e. Fin /\ -. y e. e ) -> ( ( ph /\ ( e u. { y } ) C_ A ) -> ( ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) -> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) ) ) )
193 192 a2d 
 |-  ( ( e e. Fin /\ -. y e. e ) -> ( ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) ) ) )
194 65 193 syl5 
 |-  ( ( e e. Fin /\ -. y e. e ) -> ( ( ( ph /\ e C_ A ) -> ( M gsum ( F |` e ) ) .<_ ( M gsum ( G |` e ) ) ) -> ( ( ph /\ ( e u. { y } ) C_ A ) -> ( M gsum ( F |` ( e u. { y } ) ) ) .<_ ( M gsum ( G |` ( e u. { y } ) ) ) ) ) )
195 17 25 33 41 60 194 findcard2s 
 |-  ( A e. Fin -> ( ( ph /\ A C_ A ) -> ( M gsum ( F |` A ) ) .<_ ( M gsum ( G |` A ) ) ) )
196 195 imp 
 |-  ( ( A e. Fin /\ ( ph /\ A C_ A ) ) -> ( M gsum ( F |` A ) ) .<_ ( M gsum ( G |` A ) ) )
197 9 196 mpanr2 
 |-  ( ( A e. Fin /\ ph ) -> ( M gsum ( F |` A ) ) .<_ ( M gsum ( G |` A ) ) )
198 5 197 mpancom 
 |-  ( ph -> ( M gsum ( F |` A ) ) .<_ ( M gsum ( G |` A ) ) )
199 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
200 104 199 syl 
 |-  ( ph -> ( F |` A ) = F )
201 200 oveq2d 
 |-  ( ph -> ( M gsum ( F |` A ) ) = ( M gsum F ) )
202 fnresdm 
 |-  ( G Fn A -> ( G |` A ) = G )
203 105 202 syl 
 |-  ( ph -> ( G |` A ) = G )
204 203 oveq2d 
 |-  ( ph -> ( M gsum ( G |` A ) ) = ( M gsum G ) )
205 198 201 204 3brtr3d 
 |-  ( ph -> ( M gsum F ) .<_ ( M gsum G ) )