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 ) )

Metamath Proof Explorer

Theorem gsumle

Proof