Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  gsumle Structured version   Visualization version   GIF version

Theorem gsumle 32894
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.)
Hypotheses
Ref Expression
gsumle.b 𝐵 = (Base‘𝑀)
gsumle.l = (le‘𝑀)
gsumle.m (𝜑𝑀 ∈ oMnd)
gsumle.n (𝜑𝑀 ∈ CMnd)
gsumle.a (𝜑𝐴 ∈ Fin)
gsumle.f (𝜑𝐹:𝐴𝐵)
gsumle.g (𝜑𝐺:𝐴𝐵)
gsumle.c (𝜑𝐹r 𝐺)
Assertion
Ref Expression
gsumle (𝜑 → (𝑀 Σg 𝐹) (𝑀 Σg 𝐺))

Proof of Theorem gsumle
Dummy variables 𝑒 𝑎 𝑦 𝑧 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumle.a . . 3 (𝜑𝐴 ∈ Fin)
2 ssid 3999 . . . 4 𝐴𝐴
3 sseq1 4002 . . . . . . . 8 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
43anbi2d 628 . . . . . . 7 (𝑎 = ∅ → ((𝜑𝑎𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴)))
5 reseq2 5980 . . . . . . . . 9 (𝑎 = ∅ → (𝐹𝑎) = (𝐹 ↾ ∅))
65oveq2d 7435 . . . . . . . 8 (𝑎 = ∅ → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹 ↾ ∅)))
7 reseq2 5980 . . . . . . . . 9 (𝑎 = ∅ → (𝐺𝑎) = (𝐺 ↾ ∅))
87oveq2d 7435 . . . . . . . 8 (𝑎 = ∅ → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺 ↾ ∅)))
96, 8breq12d 5162 . . . . . . 7 (𝑎 = ∅ → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅))))
104, 9imbi12d 343 . . . . . 6 (𝑎 = ∅ → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))))
11 sseq1 4002 . . . . . . . 8 (𝑎 = 𝑒 → (𝑎𝐴𝑒𝐴))
1211anbi2d 628 . . . . . . 7 (𝑎 = 𝑒 → ((𝜑𝑎𝐴) ↔ (𝜑𝑒𝐴)))
13 reseq2 5980 . . . . . . . . 9 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
1413oveq2d 7435 . . . . . . . 8 (𝑎 = 𝑒 → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹𝑒)))
15 reseq2 5980 . . . . . . . . 9 (𝑎 = 𝑒 → (𝐺𝑎) = (𝐺𝑒))
1615oveq2d 7435 . . . . . . . 8 (𝑎 = 𝑒 → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺𝑒)))
1714, 16breq12d 5162 . . . . . . 7 (𝑎 = 𝑒 → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))))
1812, 17imbi12d 343 . . . . . 6 (𝑎 = 𝑒 → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))))
19 sseq1 4002 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑎𝐴 ↔ (𝑒 ∪ {𝑦}) ⊆ 𝐴))
2019anbi2d 628 . . . . . . 7 (𝑎 = (𝑒 ∪ {𝑦}) → ((𝜑𝑎𝐴) ↔ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)))
21 reseq2 5980 . . . . . . . . 9 (𝑎 = (𝑒 ∪ {𝑦}) → (𝐹𝑎) = (𝐹 ↾ (𝑒 ∪ {𝑦})))
2221oveq2d 7435 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))))
23 reseq2 5980 . . . . . . . . 9 (𝑎 = (𝑒 ∪ {𝑦}) → (𝐺𝑎) = (𝐺 ↾ (𝑒 ∪ {𝑦})))
2423oveq2d 7435 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
2522, 24breq12d 5162 . . . . . . 7 (𝑎 = (𝑒 ∪ {𝑦}) → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))
2620, 25imbi12d 343 . . . . . 6 (𝑎 = (𝑒 ∪ {𝑦}) → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))))
27 sseq1 4002 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝐴𝐴𝐴))
2827anbi2d 628 . . . . . . 7 (𝑎 = 𝐴 → ((𝜑𝑎𝐴) ↔ (𝜑𝐴𝐴)))
29 reseq2 5980 . . . . . . . . 9 (𝑎 = 𝐴 → (𝐹𝑎) = (𝐹𝐴))
3029oveq2d 7435 . . . . . . . 8 (𝑎 = 𝐴 → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹𝐴)))
31 reseq2 5980 . . . . . . . . 9 (𝑎 = 𝐴 → (𝐺𝑎) = (𝐺𝐴))
3231oveq2d 7435 . . . . . . . 8 (𝑎 = 𝐴 → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺𝐴)))
3330, 32breq12d 5162 . . . . . . 7 (𝑎 = 𝐴 → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴))))
3428, 33imbi12d 343 . . . . . 6 (𝑎 = 𝐴 → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑𝐴𝐴) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))))
35 gsumle.m . . . . . . . . . 10 (𝜑𝑀 ∈ oMnd)
36 omndtos 32875 . . . . . . . . . 10 (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
37 tospos 18415 . . . . . . . . . 10 (𝑀 ∈ Toset → 𝑀 ∈ Poset)
3835, 36, 373syl 18 . . . . . . . . 9 (𝜑𝑀 ∈ Poset)
39 res0 5989 . . . . . . . . . . . 12 (𝐹 ↾ ∅) = ∅
4039oveq2i 7430 . . . . . . . . . . 11 (𝑀 Σg (𝐹 ↾ ∅)) = (𝑀 Σg ∅)
41 eqid 2725 . . . . . . . . . . . 12 (0g𝑀) = (0g𝑀)
4241gsum0 18647 . . . . . . . . . . 11 (𝑀 Σg ∅) = (0g𝑀)
4340, 42eqtri 2753 . . . . . . . . . 10 (𝑀 Σg (𝐹 ↾ ∅)) = (0g𝑀)
44 omndmnd 32874 . . . . . . . . . . 11 (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
45 gsumle.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑀)
4645, 41mndidcl 18712 . . . . . . . . . . 11 (𝑀 ∈ Mnd → (0g𝑀) ∈ 𝐵)
4735, 44, 463syl 18 . . . . . . . . . 10 (𝜑 → (0g𝑀) ∈ 𝐵)
4843, 47eqeltrid 2829 . . . . . . . . 9 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵)
49 gsumle.l . . . . . . . . . 10 = (le‘𝑀)
5045, 49posref 18313 . . . . . . . . 9 ((𝑀 ∈ Poset ∧ (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐹 ↾ ∅)))
5138, 48, 50syl2anc 582 . . . . . . . 8 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐹 ↾ ∅)))
52 res0 5989 . . . . . . . . . 10 (𝐺 ↾ ∅) = ∅
5339, 52eqtr4i 2756 . . . . . . . . 9 (𝐹 ↾ ∅) = (𝐺 ↾ ∅)
5453oveq2i 7430 . . . . . . . 8 (𝑀 Σg (𝐹 ↾ ∅)) = (𝑀 Σg (𝐺 ↾ ∅))
5551, 54breqtrdi 5190 . . . . . . 7 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))
5655adantr 479 . . . . . 6 ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))
57 ssun1 4170 . . . . . . . . . 10 𝑒 ⊆ (𝑒 ∪ {𝑦})
58 sstr2 3983 . . . . . . . . . 10 (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝑒 ∪ {𝑦}) ⊆ 𝐴𝑒𝐴))
5957, 58ax-mp 5 . . . . . . . . 9 ((𝑒 ∪ {𝑦}) ⊆ 𝐴𝑒𝐴)
6059anim2i 615 . . . . . . . 8 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝜑𝑒𝐴))
6160imim1i 63 . . . . . . 7 (((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))))
62 simplr 767 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴))
63 simpllr 774 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ¬ 𝑦𝑒)
64 simpr 483 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))
65 eqid 2725 . . . . . . . . . . . 12 (+g𝑀) = (+g𝑀)
6635ad3antrrr 728 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑀 ∈ oMnd)
67 gsumle.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝐴𝐵)
6867ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐺:𝐴𝐵)
69 simplr 767 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
70 ssun2 4171 . . . . . . . . . . . . . . . . 17 {𝑦} ⊆ (𝑒 ∪ {𝑦})
71 vex 3465 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
7271snss 4791 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑒 ∪ {𝑦}) ↔ {𝑦} ⊆ (𝑒 ∪ {𝑦}))
7370, 72mpbir 230 . . . . . . . . . . . . . . . 16 𝑦 ∈ (𝑒 ∪ {𝑦})
7473a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦 ∈ (𝑒 ∪ {𝑦}))
7569, 74sseldd 3977 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦𝐴)
7668, 75ffvelcdmd 7094 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑦) ∈ 𝐵)
7776adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐺𝑦) ∈ 𝐵)
78 gsumle.n . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ CMnd)
7978ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑀 ∈ CMnd)
80 vex 3465 . . . . . . . . . . . . . . 15 𝑒 ∈ V
8180a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒 ∈ V)
82 gsumle.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴𝐵)
8382ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹:𝐴𝐵)
8457, 69sstrid 3988 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒𝐴)
8583, 84fssresd 6764 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒):𝑒𝐵)
861ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐴 ∈ Fin)
87 fvexd 6911 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (0g𝑀) ∈ V)
8883, 86, 87fdmfifsupp 9400 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹 finSupp (0g𝑀))
8988, 87fsuppres 9418 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒) finSupp (0g𝑀))
9045, 41, 79, 81, 85, 89gsumcl 19882 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹𝑒)) ∈ 𝐵)
9190adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) ∈ 𝐵)
9283, 75ffvelcdmd 7094 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑦) ∈ 𝐵)
9392adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐹𝑦) ∈ 𝐵)
9468, 84fssresd 6764 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑒):𝑒𝐵)
95 ssfi 9198 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Fin ∧ 𝑒𝐴) → 𝑒 ∈ Fin)
9686, 84, 95syl2anc 582 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒 ∈ Fin)
9794, 96, 87fdmfifsupp 9400 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑒) finSupp (0g𝑀))
9845, 41, 79, 81, 94, 97gsumcl 19882 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺𝑒)) ∈ 𝐵)
9998adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐺𝑒)) ∈ 𝐵)
100 simpr 483 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))
101 simpll 765 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝜑)
102 gsumle.c . . . . . . . . . . . . . . 15 (𝜑𝐹r 𝐺)
103102ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹r 𝐺)
10482ffnd 6724 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn 𝐴)
10567ffnd 6724 . . . . . . . . . . . . . . 15 (𝜑𝐺 Fn 𝐴)
106 inidm 4217 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
107 eqidd 2726 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝐹𝑦) = (𝐹𝑦))
108 eqidd 2726 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝐺𝑦) = (𝐺𝑦))
109104, 105, 1, 1, 106, 107, 108ofrval 7697 . . . . . . . . . . . . . 14 ((𝜑𝐹r 𝐺𝑦𝐴) → (𝐹𝑦) (𝐺𝑦))
110101, 103, 75, 109syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑦) (𝐺𝑦))
111110adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐹𝑦) (𝐺𝑦))
11279adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑀 ∈ CMnd)
11345, 49, 65, 66, 77, 91, 93, 99, 100, 111, 112omndadd2d 32878 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
11496adantr 479 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑒 ∈ Fin)
11582ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝐹:𝐴𝐵)
116 simplr 767 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
117 elun1 4174 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑒𝑧 ∈ (𝑒 ∪ {𝑦}))
118117adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝑧 ∈ (𝑒 ∪ {𝑦}))
119116, 118sseldd 3977 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝑧𝐴)
120115, 119ffvelcdmd 7094 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → (𝐹𝑧) ∈ 𝐵)
121120ex 411 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑧𝑒 → (𝐹𝑧) ∈ 𝐵))
122121ad2antrr 724 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑧𝑒 → (𝐹𝑧) ∈ 𝐵))
123122imp 405 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) ∧ 𝑧𝑒) → (𝐹𝑧) ∈ 𝐵)
12471a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑦 ∈ V)
125 simplr 767 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ¬ 𝑦𝑒)
126 fveq2 6896 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
12745, 65, 112, 114, 123, 124, 125, 93, 126gsumunsn 19927 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦)))
12883, 69feqresmpt 6967 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧)))
129128oveq2d 7435 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))))
13083, 84feqresmpt 6967 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒) = (𝑧𝑒 ↦ (𝐹𝑧)))
131130oveq2d 7435 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹𝑒)) = (𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧))))
132131oveq1d 7434 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦)))
133129, 132eqeq12d 2741 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦))))
134133adantr 479 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦))))
135127, 134mpbird 256 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)))
13667adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝐺:𝐴𝐵)
137136ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → 𝐺:𝐴𝐵)
138119adantlr 713 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → 𝑧𝐴)
139137, 138ffvelcdmd 7094 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → (𝐺𝑧) ∈ 𝐵)
14071a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦 ∈ V)
141 simpr 483 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ¬ 𝑦𝑒)
142 fveq2 6896 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝐺𝑧) = (𝐺𝑦))
14345, 65, 79, 96, 139, 140, 141, 76, 142gsumunsn 19927 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦)))
144 simpr 483 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
145136, 144feqresmpt 6967 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧)))
146145oveq2d 7435 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))))
147 resabs1 6012 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒))
14857, 147mp1i 13 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒))
14959adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑒𝐴)
150136, 149feqresmpt 6967 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺𝑒) = (𝑧𝑒 ↦ (𝐺𝑧)))
151148, 150eqtrd 2765 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝑧𝑒 ↦ (𝐺𝑧)))
152151oveq2d 7435 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧))))
153 resabs1 6012 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑦} ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}))
15470, 153mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}))
15570, 144sstrid 3988 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → {𝑦} ⊆ 𝐴)
156136, 155feqresmpt 6967 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺𝑧)))
157154, 156eqtrd 2765 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺𝑧)))
158157oveq2d 7435 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺𝑧))))
15935, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ Mnd)
160159adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑀 ∈ Mnd)
16171a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ V)
16273a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ (𝑒 ∪ {𝑦}))
163144, 162sseldd 3977 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦𝐴)
164136, 163ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺𝑦) ∈ 𝐵)
165142adantl 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 = 𝑦) → (𝐺𝑧) = (𝐺𝑦))
16645, 160, 161, 164, 165gsumsnd 19919 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺𝑧))) = (𝐺𝑦))
167158, 166eqtrd 2765 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝐺𝑦))
168152, 167oveq12d 7437 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦)))
169146, 168eqeq12d 2741 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦))))
170169adantr 479 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦))))
171143, 170mpbird 256 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))))
17257, 147ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒)
173172oveq2i 7430 . . . . . . . . . . . . . . 15 (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝐺𝑒))
17470, 153ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})
175174oveq2i 7430 . . . . . . . . . . . . . . 15 (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝐺 ↾ {𝑦}))
176173, 175oveq12i 7431 . . . . . . . . . . . . . 14 ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦})))
177171, 176eqtrdi 2781 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))))
17870, 69sstrid 3988 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → {𝑦} ⊆ 𝐴)
17968, 178feqresmpt 6967 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐺𝑥)))
180179oveq2d 7435 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))))
181 cmnmnd 19764 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ CMnd → 𝑀 ∈ Mnd)
18279, 181syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑀 ∈ Mnd)
183 fveq2 6896 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
18445, 183gsumsn 19921 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ Mnd ∧ 𝑦 ∈ V ∧ (𝐺𝑦) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))) = (𝐺𝑦))
185182, 140, 76, 184syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))) = (𝐺𝑦))
186180, 185eqtrd 2765 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝐺𝑦))
187186oveq2d 7435 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
188177, 187eqtrd 2765 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
189188adantr 479 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
190113, 135, 1893brtr4d 5181 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
19162, 63, 64, 190syl21anc 836 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
192191exp31 418 . . . . . . . 8 ((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))))
193192a2d 29 . . . . . . 7 ((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) → (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))))
19461, 193syl5 34 . . . . . 6 ((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) → (((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))))
19510, 18, 26, 34, 56, 194findcard2s 9190 . . . . 5 (𝐴 ∈ Fin → ((𝜑𝐴𝐴) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴))))
196195imp 405 . . . 4 ((𝐴 ∈ Fin ∧ (𝜑𝐴𝐴)) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
1972, 196mpanr2 702 . . 3 ((𝐴 ∈ Fin ∧ 𝜑) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
1981, 197mpancom 686 . 2 (𝜑 → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
199 fnresdm 6675 . . . 4 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
200104, 199syl 17 . . 3 (𝜑 → (𝐹𝐴) = 𝐹)
201200oveq2d 7435 . 2 (𝜑 → (𝑀 Σg (𝐹𝐴)) = (𝑀 Σg 𝐹))
202 fnresdm 6675 . . . 4 (𝐺 Fn 𝐴 → (𝐺𝐴) = 𝐺)
203105, 202syl 17 . . 3 (𝜑 → (𝐺𝐴) = 𝐺)
204203oveq2d 7435 . 2 (𝜑 → (𝑀 Σg (𝐺𝐴)) = (𝑀 Σg 𝐺))
205198, 201, 2043brtr3d 5180 1 (𝜑 → (𝑀 Σg 𝐹) (𝑀 Σg 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  Vcvv 3461  cun 3942  wss 3944  c0 4322  {csn 4630   class class class wbr 5149  cmpt 5232  cres 5680   Fn wfn 6544  wf 6545  cfv 6549  (class class class)co 7419  r cofr 7684  Fincfn 8964  Basecbs 17183  +gcplusg 17236  lecple 17243  0gc0g 17424   Σg cgsu 17425  Posetcpo 18302  Tosetctos 18411  Mndcmnd 18697  CMndccmn 19747  oMndcomnd 32867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-mulcom 11204  ax-addass 11205  ax-mulass 11206  ax-distr 11207  ax-i2m1 11208  ax-1ne0 11209  ax-1rid 11210  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213  ax-pre-lttri 11214  ax-pre-lttrn 11215  ax-pre-ltadd 11216  ax-pre-mulgt0 11217
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-ofr 7686  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9388  df-oi 9535  df-card 9964  df-pnf 11282  df-mnf 11283  df-xr 11284  df-ltxr 11285  df-le 11286  df-sub 11478  df-neg 11479  df-nn 12246  df-2 12308  df-n0 12506  df-z 12592  df-uz 12856  df-fz 13520  df-fzo 13663  df-seq 14003  df-hash 14326  df-sets 17136  df-slot 17154  df-ndx 17166  df-base 17184  df-ress 17213  df-plusg 17249  df-0g 17426  df-gsum 17427  df-mre 17569  df-mrc 17570  df-acs 17572  df-proset 18290  df-poset 18308  df-toset 18412  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-submnd 18744  df-mulg 19032  df-cntz 19280  df-cmn 19749  df-omnd 32869
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator