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 31350
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 3943 . . . 4 𝐴𝐴
3 sseq1 3946 . . . . . . . 8 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
43anbi2d 629 . . . . . . 7 (𝑎 = ∅ → ((𝜑𝑎𝐴) ↔ (𝜑 ∧ ∅ ⊆ 𝐴)))
5 reseq2 5886 . . . . . . . . 9 (𝑎 = ∅ → (𝐹𝑎) = (𝐹 ↾ ∅))
65oveq2d 7291 . . . . . . . 8 (𝑎 = ∅ → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹 ↾ ∅)))
7 reseq2 5886 . . . . . . . . 9 (𝑎 = ∅ → (𝐺𝑎) = (𝐺 ↾ ∅))
87oveq2d 7291 . . . . . . . 8 (𝑎 = ∅ → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺 ↾ ∅)))
96, 8breq12d 5087 . . . . . . 7 (𝑎 = ∅ → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅))))
104, 9imbi12d 345 . . . . . 6 (𝑎 = ∅ → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))))
11 sseq1 3946 . . . . . . . 8 (𝑎 = 𝑒 → (𝑎𝐴𝑒𝐴))
1211anbi2d 629 . . . . . . 7 (𝑎 = 𝑒 → ((𝜑𝑎𝐴) ↔ (𝜑𝑒𝐴)))
13 reseq2 5886 . . . . . . . . 9 (𝑎 = 𝑒 → (𝐹𝑎) = (𝐹𝑒))
1413oveq2d 7291 . . . . . . . 8 (𝑎 = 𝑒 → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹𝑒)))
15 reseq2 5886 . . . . . . . . 9 (𝑎 = 𝑒 → (𝐺𝑎) = (𝐺𝑒))
1615oveq2d 7291 . . . . . . . 8 (𝑎 = 𝑒 → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺𝑒)))
1714, 16breq12d 5087 . . . . . . 7 (𝑎 = 𝑒 → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))))
1812, 17imbi12d 345 . . . . . 6 (𝑎 = 𝑒 → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))))
19 sseq1 3946 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑎𝐴 ↔ (𝑒 ∪ {𝑦}) ⊆ 𝐴))
2019anbi2d 629 . . . . . . 7 (𝑎 = (𝑒 ∪ {𝑦}) → ((𝜑𝑎𝐴) ↔ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)))
21 reseq2 5886 . . . . . . . . 9 (𝑎 = (𝑒 ∪ {𝑦}) → (𝐹𝑎) = (𝐹 ↾ (𝑒 ∪ {𝑦})))
2221oveq2d 7291 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))))
23 reseq2 5886 . . . . . . . . 9 (𝑎 = (𝑒 ∪ {𝑦}) → (𝐺𝑎) = (𝐺 ↾ (𝑒 ∪ {𝑦})))
2423oveq2d 7291 . . . . . . . 8 (𝑎 = (𝑒 ∪ {𝑦}) → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))
2522, 24breq12d 5087 . . . . . . 7 (𝑎 = (𝑒 ∪ {𝑦}) → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦})))))
2620, 25imbi12d 345 . . . . . 6 (𝑎 = (𝑒 ∪ {𝑦}) → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))))))
27 sseq1 3946 . . . . . . . 8 (𝑎 = 𝐴 → (𝑎𝐴𝐴𝐴))
2827anbi2d 629 . . . . . . 7 (𝑎 = 𝐴 → ((𝜑𝑎𝐴) ↔ (𝜑𝐴𝐴)))
29 reseq2 5886 . . . . . . . . 9 (𝑎 = 𝐴 → (𝐹𝑎) = (𝐹𝐴))
3029oveq2d 7291 . . . . . . . 8 (𝑎 = 𝐴 → (𝑀 Σg (𝐹𝑎)) = (𝑀 Σg (𝐹𝐴)))
31 reseq2 5886 . . . . . . . . 9 (𝑎 = 𝐴 → (𝐺𝑎) = (𝐺𝐴))
3231oveq2d 7291 . . . . . . . 8 (𝑎 = 𝐴 → (𝑀 Σg (𝐺𝑎)) = (𝑀 Σg (𝐺𝐴)))
3330, 32breq12d 5087 . . . . . . 7 (𝑎 = 𝐴 → ((𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎)) ↔ (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴))))
3428, 33imbi12d 345 . . . . . 6 (𝑎 = 𝐴 → (((𝜑𝑎𝐴) → (𝑀 Σg (𝐹𝑎)) (𝑀 Σg (𝐺𝑎))) ↔ ((𝜑𝐴𝐴) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))))
35 gsumle.m . . . . . . . . . 10 (𝜑𝑀 ∈ oMnd)
36 omndtos 31331 . . . . . . . . . 10 (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
37 tospos 18138 . . . . . . . . . 10 (𝑀 ∈ Toset → 𝑀 ∈ Poset)
3835, 36, 373syl 18 . . . . . . . . 9 (𝜑𝑀 ∈ Poset)
39 res0 5895 . . . . . . . . . . . 12 (𝐹 ↾ ∅) = ∅
4039oveq2i 7286 . . . . . . . . . . 11 (𝑀 Σg (𝐹 ↾ ∅)) = (𝑀 Σg ∅)
41 eqid 2738 . . . . . . . . . . . 12 (0g𝑀) = (0g𝑀)
4241gsum0 18368 . . . . . . . . . . 11 (𝑀 Σg ∅) = (0g𝑀)
4340, 42eqtri 2766 . . . . . . . . . 10 (𝑀 Σg (𝐹 ↾ ∅)) = (0g𝑀)
44 omndmnd 31330 . . . . . . . . . . 11 (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
45 gsumle.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑀)
4645, 41mndidcl 18400 . . . . . . . . . . 11 (𝑀 ∈ Mnd → (0g𝑀) ∈ 𝐵)
4735, 44, 463syl 18 . . . . . . . . . 10 (𝜑 → (0g𝑀) ∈ 𝐵)
4843, 47eqeltrid 2843 . . . . . . . . 9 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵)
49 gsumle.l . . . . . . . . . 10 = (le‘𝑀)
5045, 49posref 18036 . . . . . . . . 9 ((𝑀 ∈ Poset ∧ (𝑀 Σg (𝐹 ↾ ∅)) ∈ 𝐵) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐹 ↾ ∅)))
5138, 48, 50syl2anc 584 . . . . . . . 8 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐹 ↾ ∅)))
52 res0 5895 . . . . . . . . . 10 (𝐺 ↾ ∅) = ∅
5339, 52eqtr4i 2769 . . . . . . . . 9 (𝐹 ↾ ∅) = (𝐺 ↾ ∅)
5453oveq2i 7286 . . . . . . . 8 (𝑀 Σg (𝐹 ↾ ∅)) = (𝑀 Σg (𝐺 ↾ ∅))
5551, 54breqtrdi 5115 . . . . . . 7 (𝜑 → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))
5655adantr 481 . . . . . 6 ((𝜑 ∧ ∅ ⊆ 𝐴) → (𝑀 Σg (𝐹 ↾ ∅)) (𝑀 Σg (𝐺 ↾ ∅)))
57 ssun1 4106 . . . . . . . . . 10 𝑒 ⊆ (𝑒 ∪ {𝑦})
58 sstr2 3928 . . . . . . . . . 10 (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝑒 ∪ {𝑦}) ⊆ 𝐴𝑒𝐴))
5957, 58ax-mp 5 . . . . . . . . 9 ((𝑒 ∪ {𝑦}) ⊆ 𝐴𝑒𝐴)
6059anim2i 617 . . . . . . . 8 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝜑𝑒𝐴))
6160imim1i 63 . . . . . . 7 (((𝜑𝑒𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))))
62 simplr 766 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴))
63 simpllr 773 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ¬ 𝑦𝑒)
64 simpr 485 . . . . . . . . . 10 ((((𝑒 ∈ Fin ∧ ¬ 𝑦𝑒) ∧ (𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴)) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))
65 eqid 2738 . . . . . . . . . . . 12 (+g𝑀) = (+g𝑀)
6635ad3antrrr 727 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑀 ∈ oMnd)
67 gsumle.g . . . . . . . . . . . . . . 15 (𝜑𝐺:𝐴𝐵)
6867ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐺:𝐴𝐵)
69 simplr 766 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
70 ssun2 4107 . . . . . . . . . . . . . . . . 17 {𝑦} ⊆ (𝑒 ∪ {𝑦})
71 vex 3436 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
7271snss 4719 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ (𝑒 ∪ {𝑦}) ↔ {𝑦} ⊆ (𝑒 ∪ {𝑦}))
7370, 72mpbir 230 . . . . . . . . . . . . . . . 16 𝑦 ∈ (𝑒 ∪ {𝑦})
7473a1i 11 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦 ∈ (𝑒 ∪ {𝑦}))
7569, 74sseldd 3922 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦𝐴)
7668, 75ffvelrnd 6962 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑦) ∈ 𝐵)
7776adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐺𝑦) ∈ 𝐵)
78 gsumle.n . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ CMnd)
7978ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑀 ∈ CMnd)
80 vex 3436 . . . . . . . . . . . . . . 15 𝑒 ∈ V
8180a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒 ∈ V)
82 gsumle.f . . . . . . . . . . . . . . . 16 (𝜑𝐹:𝐴𝐵)
8382ad2antrr 723 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹:𝐴𝐵)
8457, 69sstrid 3932 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒𝐴)
8583, 84fssresd 6641 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒):𝑒𝐵)
861ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐴 ∈ Fin)
87 fvexd 6789 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (0g𝑀) ∈ V)
8883, 86, 87fdmfifsupp 9138 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹 finSupp (0g𝑀))
8988, 87fsuppres 9153 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒) finSupp (0g𝑀))
9045, 41, 79, 81, 85, 89gsumcl 19516 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹𝑒)) ∈ 𝐵)
9190adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) ∈ 𝐵)
9283, 75ffvelrnd 6962 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑦) ∈ 𝐵)
9392adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐹𝑦) ∈ 𝐵)
9468, 84fssresd 6641 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑒):𝑒𝐵)
95 ssfi 8956 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Fin ∧ 𝑒𝐴) → 𝑒 ∈ Fin)
9686, 84, 95syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑒 ∈ Fin)
9794, 96, 87fdmfifsupp 9138 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺𝑒) finSupp (0g𝑀))
9845, 41, 79, 81, 94, 97gsumcl 19516 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺𝑒)) ∈ 𝐵)
9998adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐺𝑒)) ∈ 𝐵)
100 simpr 485 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒)))
101 simpll 764 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝜑)
102 gsumle.c . . . . . . . . . . . . . . 15 (𝜑𝐹r 𝐺)
103102ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝐹r 𝐺)
10482ffnd 6601 . . . . . . . . . . . . . . 15 (𝜑𝐹 Fn 𝐴)
10567ffnd 6601 . . . . . . . . . . . . . . 15 (𝜑𝐺 Fn 𝐴)
106 inidm 4152 . . . . . . . . . . . . . . 15 (𝐴𝐴) = 𝐴
107 eqidd 2739 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝐹𝑦) = (𝐹𝑦))
108 eqidd 2739 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝐺𝑦) = (𝐺𝑦))
109104, 105, 1, 1, 106, 107, 108ofrval 7545 . . . . . . . . . . . . . 14 ((𝜑𝐹r 𝐺𝑦𝐴) → (𝐹𝑦) (𝐺𝑦))
110101, 103, 75, 109syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑦) (𝐺𝑦))
111110adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝐹𝑦) (𝐺𝑦))
11279adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑀 ∈ CMnd)
11345, 49, 65, 66, 77, 91, 93, 99, 100, 111, 112omndadd2d 31334 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
11496adantr 481 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑒 ∈ Fin)
11582ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝐹:𝐴𝐵)
116 simplr 766 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
117 elun1 4110 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑒𝑧 ∈ (𝑒 ∪ {𝑦}))
118117adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝑧 ∈ (𝑒 ∪ {𝑦}))
119116, 118sseldd 3922 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → 𝑧𝐴)
120115, 119ffvelrnd 6962 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧𝑒) → (𝐹𝑧) ∈ 𝐵)
121120ex 413 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑧𝑒 → (𝐹𝑧) ∈ 𝐵))
122121ad2antrr 723 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑧𝑒 → (𝐹𝑧) ∈ 𝐵))
123122imp 407 . . . . . . . . . . . . 13 (((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) ∧ 𝑧𝑒) → (𝐹𝑧) ∈ 𝐵)
12471a1i 11 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → 𝑦 ∈ V)
125 simplr 766 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ¬ 𝑦𝑒)
126 fveq2 6774 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
12745, 65, 112, 114, 123, 124, 125, 93, 126gsumunsn 19561 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦)))
12883, 69feqresmpt 6838 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧)))
129128oveq2d 7291 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))))
13083, 84feqresmpt 6838 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐹𝑒) = (𝑧𝑒 ↦ (𝐹𝑧)))
131130oveq2d 7291 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐹𝑒)) = (𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧))))
132131oveq1d 7290 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦)))
133129, 132eqeq12d 2754 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦))))
134133adantr 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → ((𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐹𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐹𝑧)))(+g𝑀)(𝐹𝑦))))
135127, 134mpbird 256 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐹 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐹𝑒))(+g𝑀)(𝐹𝑦)))
13667adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝐺:𝐴𝐵)
137136ad2antrr 723 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → 𝐺:𝐴𝐵)
138119adantlr 712 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → 𝑧𝐴)
139137, 138ffvelrnd 6962 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ 𝑧𝑒) → (𝐺𝑧) ∈ 𝐵)
14071a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑦 ∈ V)
141 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ¬ 𝑦𝑒)
142 fveq2 6774 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝐺𝑧) = (𝐺𝑦))
14345, 65, 79, 96, 139, 140, 141, 76, 142gsumunsn 19561 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦)))
144 simpr 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑒 ∪ {𝑦}) ⊆ 𝐴)
145136, 144feqresmpt 6838 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ (𝑒 ∪ {𝑦})) = (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧)))
146145oveq2d 7291 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))))
147 resabs1 5921 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒))
14857, 147mp1i 13 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒))
14959adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑒𝐴)
150136, 149feqresmpt 6838 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺𝑒) = (𝑧𝑒 ↦ (𝐺𝑧)))
151148, 150eqtrd 2778 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝑧𝑒 ↦ (𝐺𝑧)))
152151oveq2d 7291 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧))))
153 resabs1 5921 . . . . . . . . . . . . . . . . . . . . . 22 ({𝑦} ⊆ (𝑒 ∪ {𝑦}) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}))
15470, 153mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦}))
15570, 144sstrid 3932 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → {𝑦} ⊆ 𝐴)
156136, 155feqresmpt 6838 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺 ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺𝑧)))
157154, 156eqtrd 2778 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝑧 ∈ {𝑦} ↦ (𝐺𝑧)))
158157oveq2d 7291 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺𝑧))))
15935, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝑀 ∈ Mnd)
160159adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑀 ∈ Mnd)
16171a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ V)
16273a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦 ∈ (𝑒 ∪ {𝑦}))
163144, 162sseldd 3922 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → 𝑦𝐴)
164136, 163ffvelrnd 6962 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝐺𝑦) ∈ 𝐵)
165142adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ 𝑧 = 𝑦) → (𝐺𝑧) = (𝐺𝑦))
16645, 160, 161, 164, 165gsumsnd 19553 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg (𝑧 ∈ {𝑦} ↦ (𝐺𝑧))) = (𝐺𝑦))
167158, 166eqtrd 2778 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝐺𝑦))
168152, 167oveq12d 7293 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦)))
169146, 168eqeq12d 2754 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦))))
170169adantr 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) ↔ (𝑀 Σg (𝑧 ∈ (𝑒 ∪ {𝑦}) ↦ (𝐺𝑧))) = ((𝑀 Σg (𝑧𝑒 ↦ (𝐺𝑧)))(+g𝑀)(𝐺𝑦))))
171143, 170mpbird 256 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))))
17257, 147ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒) = (𝐺𝑒)
173172oveq2i 7286 . . . . . . . . . . . . . . 15 (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒)) = (𝑀 Σg (𝐺𝑒))
17470, 153ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}) = (𝐺 ↾ {𝑦})
175174oveq2i 7286 . . . . . . . . . . . . . . 15 (𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦})) = (𝑀 Σg (𝐺 ↾ {𝑦}))
176173, 175oveq12i 7287 . . . . . . . . . . . . . 14 ((𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ 𝑒))(+g𝑀)(𝑀 Σg ((𝐺 ↾ (𝑒 ∪ {𝑦})) ↾ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦})))
177171, 176eqtrdi 2794 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))))
17870, 69sstrid 3932 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → {𝑦} ⊆ 𝐴)
17968, 178feqresmpt 6838 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝐺 ↾ {𝑦}) = (𝑥 ∈ {𝑦} ↦ (𝐺𝑥)))
180179oveq2d 7291 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))))
181 cmnmnd 19402 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ CMnd → 𝑀 ∈ Mnd)
18279, 181syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → 𝑀 ∈ Mnd)
183 fveq2 6774 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (𝐺𝑥) = (𝐺𝑦))
18445, 183gsumsn 19555 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ Mnd ∧ 𝑦 ∈ V ∧ (𝐺𝑦) ∈ 𝐵) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))) = (𝐺𝑦))
185182, 140, 76, 184syl3anc 1370 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝑥 ∈ {𝑦} ↦ (𝐺𝑥))) = (𝐺𝑦))
186180, 185eqtrd 2778 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ {𝑦})) = (𝐺𝑦))
187186oveq2d 7291 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝑀 Σg (𝐺 ↾ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
188177, 187eqtrd 2778 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
189188adantr 481 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 ∪ {𝑦}) ⊆ 𝐴) ∧ ¬ 𝑦𝑒) ∧ (𝑀 Σg (𝐹𝑒)) (𝑀 Σg (𝐺𝑒))) → (𝑀 Σg (𝐺 ↾ (𝑒 ∪ {𝑦}))) = ((𝑀 Σg (𝐺𝑒))(+g𝑀)(𝐺𝑦)))
190113, 135, 1893brtr4d 5106 . . . . . . . . . 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 8948 . . . . 5 (𝐴 ∈ Fin → ((𝜑𝐴𝐴) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴))))
196195imp 407 . . . 4 ((𝐴 ∈ Fin ∧ (𝜑𝐴𝐴)) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
1972, 196mpanr2 701 . . 3 ((𝐴 ∈ Fin ∧ 𝜑) → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
1981, 197mpancom 685 . 2 (𝜑 → (𝑀 Σg (𝐹𝐴)) (𝑀 Σg (𝐺𝐴)))
199 fnresdm 6551 . . . 4 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
200104, 199syl 17 . . 3 (𝜑 → (𝐹𝐴) = 𝐹)
201200oveq2d 7291 . 2 (𝜑 → (𝑀 Σg (𝐹𝐴)) = (𝑀 Σg 𝐹))
202 fnresdm 6551 . . . 4 (𝐺 Fn 𝐴 → (𝐺𝐴) = 𝐺)
203105, 202syl 17 . . 3 (𝜑 → (𝐺𝐴) = 𝐺)
204203oveq2d 7291 . 2 (𝜑 → (𝑀 Σg (𝐺𝐴)) = (𝑀 Σg 𝐺))
205198, 201, 2043brtr3d 5105 1 (𝜑 → (𝑀 Σg 𝐹) (𝑀 Σg 𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  Vcvv 3432  cun 3885  wss 3887  c0 4256  {csn 4561   class class class wbr 5074  cmpt 5157  cres 5591   Fn wfn 6428  wf 6429  cfv 6433  (class class class)co 7275  r cofr 7532  Fincfn 8733  Basecbs 16912  +gcplusg 16962  lecple 16969  0gc0g 17150   Σg cgsu 17151  Posetcpo 18025  Tosetctos 18134  Mndcmnd 18385  CMndccmn 19386  oMndcomnd 31323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-of 7533  df-ofr 7534  df-om 7713  df-1st 7831  df-2nd 7832  df-supp 7978  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-fsupp 9129  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974  df-2 12036  df-n0 12234  df-z 12320  df-uz 12583  df-fz 13240  df-fzo 13383  df-seq 13722  df-hash 14045  df-sets 16865  df-slot 16883  df-ndx 16895  df-base 16913  df-ress 16942  df-plusg 16975  df-0g 17152  df-gsum 17153  df-mre 17295  df-mrc 17296  df-acs 17298  df-proset 18013  df-poset 18031  df-toset 18135  df-mgm 18326  df-sgrp 18375  df-mnd 18386  df-submnd 18431  df-mulg 18701  df-cntz 18923  df-cmn 19388  df-omnd 31325
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator