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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
gsumle.l ⊢ ≤ = ( le ‘ 𝑀 )
gsumle.m ⊢ ( 𝜑 → 𝑀 ∈ oMnd )
gsumle.n ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
gsumle.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsumle.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumle.g ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
gsumle.c ⊢ ( 𝜑 → 𝐹 ∘r ≤ 𝐺 )
Assertion gsumle ( 𝜑 → ( 𝑀 Σg 𝐹 ) ≤ ( 𝑀 Σg 𝐺 ) )

Proof

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