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 30639
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 3993 . . . 4 𝐴𝐴
3 sseq1 3996 . . . . . . . 8 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
43anbi2d 628 . . . . . . 7 (𝑎 = ∅ → ((𝜑𝑎𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴)))
5 reseq2 5847 . . . . . . . . 9 (𝑎 = ∅ → (𝐹𝑎) = (𝐹 ↾ ∅))
65oveq2d 7164 . . . . . . . 8 (𝑎 = ∅ → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹 ↾ ∅)))
7 reseq2 5847 . . . . . . . . 9 (𝑎 = ∅ → (𝐺𝑎) = (𝐺 ↾ ∅))
87oveq2d 7164 . . . . . . . 8 (𝑎 = ∅ → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺 ↾ ∅)))
96, 8breq12d 5076 . . . . . . 7 (𝑎 = ∅ → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅))))
104, 9imbi12d 346 . . . . . 6 (𝑎 = ∅ → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))))
11 sseq1 3996 . . . . . . . 8 (𝑎 = 𝑒 → (𝑎𝐴𝑒𝐴))
1211anbi2d 628 . . . . . . 7 (𝑎 = 𝑒 → ((𝜑𝑎𝐴) ↔ (𝜑𝑒𝐴)))
13 reseq2 5847 . . . . . . . . 9 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
1413oveq2d 7164 . . . . . . . 8 (𝑎 = 𝑒 → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹𝑒)))
15 reseq2 5847 . . . . . . . . 9 (𝑎 = 𝑒 → (𝐺𝑎) = (𝐺𝑒))
1615oveq2d 7164 . . . . . . . 8 (𝑎 = 𝑒 → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺𝑒)))
1714, 16breq12d 5076 . . . . . . 7 (𝑎 = 𝑒 → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))))
1812, 17imbi12d 346 . . . . . 6 (𝑎 = 𝑒 → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))))
19 sseq1 3996 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑎𝐴 ↔ (𝑒 ∪ {𝑦}) ⊆ 𝐴))
2019anbi2d 628 . . . . . . 7 (𝑎 = (𝑒 ∪ {𝑦}) → ((𝜑𝑎𝐴) ↔ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)))
21 reseq2 5847 . . . . . . . . 9 (𝑎 = (𝑒 ∪ {𝑦}) → (𝐹𝑎) = (𝐹 ↾ (𝑒 ∪ {𝑦})))
2221oveq2d 7164 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))))
23 reseq2 5847 . . . . . . . . 9 (𝑎 = (𝑒 ∪ {𝑦}) → (𝐺𝑎) = (𝐺 ↾ (𝑒 ∪ {𝑦})))
2423oveq2d 7164 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
2522, 24breq12d 5076 . . . . . . 7 (𝑎 = (𝑒 ∪ {𝑦}) → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))
2620, 25imbi12d 346 . . . . . 6 (𝑎 = (𝑒 ∪ {𝑦}) → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))))
27 sseq1 3996 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝐴𝐴𝐴))
2827anbi2d 628 . . . . . . 7 (𝑎 = 𝐴 → ((𝜑𝑎𝐴) ↔ (𝜑𝐴𝐴)))
29 reseq2 5847 . . . . . . . . 9 (𝑎 = 𝐴 → (𝐹𝑎) = (𝐹𝐴))
3029oveq2d 7164 . . . . . . . 8 (𝑎 = 𝐴 → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹𝐴)))
31 reseq2 5847 . . . . . . . . 9 (𝑎 = 𝐴 → (𝐺𝑎) = (𝐺𝐴))
3231oveq2d 7164 . . . . . . . 8 (𝑎 = 𝐴 → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺𝐴)))
3330, 32breq12d 5076 . . . . . . 7 (𝑎 = 𝐴 → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴))))
3428, 33imbi12d 346 . . . . . 6 (𝑎 = 𝐴 → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑𝐴𝐴) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))))
35 gsumle.m . . . . . . . . . 10 (𝜑𝑀 ∈ oMnd)
36 omndtos 30620 . . . . . . . . . 10 (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
37 tospos 30559 . . . . . . . . . 10 (𝑀 ∈ Toset → 𝑀 ∈ Poset)
3835, 36, 373syl 18 . . . . . . . . 9 (𝜑𝑀 ∈ Poset)
39 res0 5856 . . . . . . . . . . . 12 (𝐹 ↾ ∅) = ∅
4039oveq2i 7159 . . . . . . . . . . 11 (𝑀 Σg (𝐹 ↾ ∅)) = (𝑀 Σg ∅)
41 eqid 2826 . . . . . . . . . . . 12 (0g𝑀) = (0g𝑀)
4241gsum0 17883 . . . . . . . . . . 11 (𝑀 Σg ∅) = (0g𝑀)
4340, 42eqtri 2849 . . . . . . . . . 10 (𝑀 Σg (𝐹 ↾ ∅)) = (0g𝑀)
44 omndmnd 30619 . . . . . . . . . . 11 (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
45 gsumle.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑀)
4645, 41mndidcl 17914 . . . . . . . . . . 11 (𝑀 ∈ Mnd → (0g𝑀) ∈ 𝐵)
4735, 44, 463syl 18 . . . . . . . . . 10 (𝜑 → (0g𝑀) ∈ 𝐵)
4843, 47eqeltrid 2922 . . . . . . . . 9 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵)
49 gsumle.l . . . . . . . . . 10 = (le‘𝑀)
5045, 49posref 17551 . . . . . . . . 9 ((𝑀 ∈ Poset ∧ (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐹 ↾ ∅)))
5138, 48, 50syl2anc 584 . . . . . . . 8 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐹 ↾ ∅)))
52 res0 5856 . . . . . . . . . 10 (𝐺 ↾ ∅) = ∅
5339, 52eqtr4i 2852 . . . . . . . . 9 (𝐹 ↾ ∅) = (𝐺 ↾ ∅)
5453oveq2i 7159 . . . . . . . 8 (𝑀 Σg (𝐹 ↾ ∅)) = (𝑀 Σg (𝐺 ↾ ∅))
5551, 54breqtrdi 5104 . . . . . . 7 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))
5655adantr 481 . . . . . 6 ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))
57 ssun1 4152 . . . . . . . . . 10 𝑒 ⊆ (𝑒 ∪ {𝑦})
58 sstr2 3978 . . . . . . . . . 10 (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝑒 ∪ {𝑦}) ⊆ 𝐴𝑒𝐴))
5957, 58ax-mp 5 . . . . . . . . 9 ((𝑒 ∪ {𝑦}) ⊆ 𝐴𝑒𝐴)
6059anim2i 616 . . . . . . . 8 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝜑𝑒𝐴))
6160imim1i 63 . . . . . . 7 (((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))))
62 simplr 765 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴))
63 simpllr 772 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ¬ 𝑦𝑒)
64 simpr 485 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))
65 eqid 2826 . . . . . . . . . . . 12 (+g𝑀) = (+g𝑀)
6635ad3antrrr 726 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑀 ∈ oMnd)
67 gsumle.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝐴𝐵)
6867ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐺:𝐴𝐵)
69 simplr 765 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
70 ssun2 4153 . . . . . . . . . . . . . . . . 17 {𝑦} ⊆ (𝑒 ∪ {𝑦})
71 vex 3503 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
7271snss 4717 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑒 ∪ {𝑦}) ↔ {𝑦} ⊆ (𝑒 ∪ {𝑦}))
7370, 72mpbir 232 . . . . . . . . . . . . . . . 16 𝑦 ∈ (𝑒 ∪ {𝑦})
7473a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦 ∈ (𝑒 ∪ {𝑦}))
7569, 74sseldd 3972 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦𝐴)
7668, 75ffvelrnd 6848 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑦) ∈ 𝐵)
7776adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐺𝑦) ∈ 𝐵)
78 gsumle.n . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ CMnd)
7978ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑀 ∈ CMnd)
80 vex 3503 . . . . . . . . . . . . . . 15 𝑒 ∈ V
8180a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒 ∈ V)
82 gsumle.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴𝐵)
8382ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹:𝐴𝐵)
8457, 69sstrid 3982 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒𝐴)
8583, 84fssresd 6542 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒):𝑒𝐵)
861ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐴 ∈ Fin)
87 fvexd 6682 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (0g𝑀) ∈ V)
8883, 86, 87fdmfifsupp 8832 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹 finSupp (0g𝑀))
8988, 87fsuppres 8847 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒) finSupp (0g𝑀))
9045, 41, 79, 81, 85, 89gsumcl 18955 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹𝑒)) ∈ 𝐵)
9190adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) ∈ 𝐵)
9283, 75ffvelrnd 6848 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑦) ∈ 𝐵)
9392adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐹𝑦) ∈ 𝐵)
9468, 84fssresd 6542 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑒):𝑒𝐵)
95 ssfi 8727 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Fin ∧ 𝑒𝐴) → 𝑒 ∈ Fin)
9686, 84, 95syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒 ∈ Fin)
9794, 96, 87fdmfifsupp 8832 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑒) finSupp (0g𝑀))
9845, 41, 79, 81, 94, 97gsumcl 18955 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺𝑒)) ∈ 𝐵)
9998adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐺𝑒)) ∈ 𝐵)
100 simpr 485 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))
101 simpll 763 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝜑)
102 gsumle.c . . . . . . . . . . . . . . 15 (𝜑𝐹r 𝐺)
103102ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹r 𝐺)
10482ffnd 6512 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn 𝐴)
10567ffnd 6512 . . . . . . . . . . . . . . 15 (𝜑𝐺 Fn 𝐴)
106 inidm 4199 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
107 eqidd 2827 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝐹𝑦) = (𝐹𝑦))
108 eqidd 2827 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝐺𝑦) = (𝐺𝑦))
109104, 105, 1, 1, 106, 107, 108ofrval 7409 . . . . . . . . . . . . . 14 ((𝜑𝐹r 𝐺𝑦𝐴) → (𝐹𝑦) (𝐺𝑦))
110101, 103, 75, 109syl3anc 1365 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑦) (𝐺𝑦))
111110adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐹𝑦) (𝐺𝑦))
11279adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑀 ∈ CMnd)
11345, 49, 65, 66, 77, 91, 93, 99, 100, 111, 112omndadd2d 30623 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
11496adantr 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑒 ∈ Fin)
11582ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝐹:𝐴𝐵)
116 simplr 765 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
117 elun1 4156 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑒𝑧 ∈ (𝑒 ∪ {𝑦}))
118117adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝑧 ∈ (𝑒 ∪ {𝑦}))
119116, 118sseldd 3972 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝑧𝐴)
120115, 119ffvelrnd 6848 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → (𝐹𝑧) ∈ 𝐵)
121120ex 413 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑧𝑒 → (𝐹𝑧) ∈ 𝐵))
122121ad2antrr 722 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑧𝑒 → (𝐹𝑧) ∈ 𝐵))
123122imp 407 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) ∧ 𝑧𝑒) → (𝐹𝑧) ∈ 𝐵)
12471a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑦 ∈ V)
125 simplr 765 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ¬ 𝑦𝑒)
126 fveq2 6667 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
12745, 65, 112, 114, 123, 124, 125, 93, 126gsumunsn 19000 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦)))
12883, 69feqresmpt 6731 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧)))
129128oveq2d 7164 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))))
13083, 84feqresmpt 6731 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒) = (𝑧𝑒 ↦ (𝐹𝑧)))
131130oveq2d 7164 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹𝑒)) = (𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧))))
132131oveq1d 7163 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦)))
133129, 132eqeq12d 2842 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦))))
134133adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦))))
135127, 134mpbird 258 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)))
13667adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝐺:𝐴𝐵)
137136ad2antrr 722 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → 𝐺:𝐴𝐵)
138119adantlr 711 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → 𝑧𝐴)
139137, 138ffvelrnd 6848 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → (𝐺𝑧) ∈ 𝐵)
14071a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦 ∈ V)
141 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ¬ 𝑦𝑒)
142 fveq2 6667 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝐺𝑧) = (𝐺𝑦))
14345, 65, 79, 96, 139, 140, 141, 76, 142gsumunsn 19000 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦)))
144 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
145136, 144feqresmpt 6731 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧)))
146145oveq2d 7164 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))))
147 resabs1 5882 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒))
14857, 147mp1i 13 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒))
14959adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑒𝐴)
150136, 149feqresmpt 6731 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺𝑒) = (𝑧𝑒 ↦ (𝐺𝑧)))
151148, 150eqtrd 2861 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝑧𝑒 ↦ (𝐺𝑧)))
152151oveq2d 7164 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧))))
153 resabs1 5882 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑦} ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}))
15470, 153mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}))
15570, 144sstrid 3982 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → {𝑦} ⊆ 𝐴)
156136, 155feqresmpt 6731 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺𝑧)))
157154, 156eqtrd 2861 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺𝑧)))
158157oveq2d 7164 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺𝑧))))
15935, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ Mnd)
160159adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑀 ∈ Mnd)
16171a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ V)
16273a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ (𝑒 ∪ {𝑦}))
163144, 162sseldd 3972 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦𝐴)
164136, 163ffvelrnd 6848 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺𝑦) ∈ 𝐵)
165142adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 = 𝑦) → (𝐺𝑧) = (𝐺𝑦))
16645, 160, 161, 164, 165gsumsnd 18992 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺𝑧))) = (𝐺𝑦))
167158, 166eqtrd 2861 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝐺𝑦))
168152, 167oveq12d 7166 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦)))
169146, 168eqeq12d 2842 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦))))
170169adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦))))
171143, 170mpbird 258 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))))
17257, 147ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒)
173172oveq2i 7159 . . . . . . . . . . . . . . 15 (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝐺𝑒))
17470, 153ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})
175174oveq2i 7159 . . . . . . . . . . . . . . 15 (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝐺 ↾ {𝑦}))
176173, 175oveq12i 7160 . . . . . . . . . . . . . 14 ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦})))
177171, 176syl6eq 2877 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))))
17870, 69sstrid 3982 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → {𝑦} ⊆ 𝐴)
17968, 178feqresmpt 6731 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐺𝑥)))
180179oveq2d 7164 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))))
181 cmnmnd 18842 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ CMnd → 𝑀 ∈ Mnd)
18279, 181syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑀 ∈ Mnd)
183 fveq2 6667 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
18445, 183gsumsn 18994 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ Mnd ∧ 𝑦 ∈ V ∧ (𝐺𝑦) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))) = (𝐺𝑦))
185182, 140, 76, 184syl3anc 1365 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))) = (𝐺𝑦))
186180, 185eqtrd 2861 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝐺𝑦))
187186oveq2d 7164 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
188177, 187eqtrd 2861 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
189188adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
190113, 135, 1893brtr4d 5095 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
19162, 63, 64, 190syl21anc 835 . . . . . . . . 9 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
192191exp31 420 . . . . . . . 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 8748 . . . . 5 (𝐴 ∈ Fin → ((𝜑𝐴𝐴) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴))))
196195imp 407 . . . 4 ((𝐴 ∈ Fin ∧ (𝜑𝐴𝐴)) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
1972, 196mpanr2 700 . . 3 ((𝐴 ∈ Fin ∧ 𝜑) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
1981, 197mpancom 684 . 2 (𝜑 → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
199 fnresdm 6463 . . . 4 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
200104, 199syl 17 . . 3 (𝜑 → (𝐹𝐴) = 𝐹)
201200oveq2d 7164 . 2 (𝜑 → (𝑀 Σg (𝐹𝐴)) = (𝑀 Σg 𝐹))
202 fnresdm 6463 . . . 4 (𝐺 Fn 𝐴 → (𝐺𝐴) = 𝐺)
203105, 202syl 17 . . 3 (𝜑 → (𝐺𝐴) = 𝐺)
204203oveq2d 7164 . 2 (𝜑 → (𝑀 Σg (𝐺𝐴)) = (𝑀 Σg 𝐺))
205198, 201, 2043brtr3d 5094 1 (𝜑 → (𝑀 Σg 𝐹) (𝑀 Σg 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1530  wcel 2107  Vcvv 3500  cun 3938  wss 3940  c0 4295  {csn 4564   class class class wbr 5063  cmpt 5143  cres 5556   Fn wfn 6347  wf 6348  cfv 6352  (class class class)co 7148  r cofr 7398  Fincfn 8498  Basecbs 16473  +gcplusg 16555  lecple 16562  0gc0g 16703   Σg cgsu 16704  Posetcpo 17540  Tosetctos 17633  Mndcmnd 17900  CMndccmn 18826  oMndcomnd 30612
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-isom 6361  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-of 7399  df-ofr 7400  df-om 7569  df-1st 7680  df-2nd 7681  df-supp 7822  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-oadd 8097  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-fsupp 8823  df-oi 8963  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-n0 11887  df-z 11971  df-uz 12233  df-fz 12883  df-fzo 13024  df-seq 13360  df-hash 13681  df-ndx 16476  df-slot 16477  df-base 16479  df-sets 16480  df-ress 16481  df-plusg 16568  df-0g 16705  df-gsum 16706  df-mre 16847  df-mrc 16848  df-acs 16850  df-proset 17528  df-poset 17546  df-toset 17634  df-mgm 17842  df-sgrp 17890  df-mnd 17901  df-submnd 17945  df-mulg 18155  df-cntz 18377  df-cmn 18828  df-omnd 30614
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator