MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsum2dlem2 Structured version   Visualization version   GIF version

Theorem gsum2dlem2 19070
Description: Lemma for gsum2d 19071. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.)
Hypotheses
Ref Expression
gsum2d.b 𝐵 = (Base‘𝐺)
gsum2d.z 0 = (0g𝐺)
gsum2d.g (𝜑𝐺 ∈ CMnd)
gsum2d.a (𝜑𝐴𝑉)
gsum2d.r (𝜑 → Rel 𝐴)
gsum2d.d (𝜑𝐷𝑊)
gsum2d.s (𝜑 → dom 𝐴𝐷)
gsum2d.f (𝜑𝐹:𝐴𝐵)
gsum2d.w (𝜑𝐹 finSupp 0 )
Assertion
Ref Expression
gsum2dlem2 (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
Distinct variable groups:   𝑗,𝑘,𝐴   𝑗,𝐹,𝑘   𝑗,𝐺,𝑘   𝜑,𝑗,𝑘   𝐵,𝑗,𝑘   𝐷,𝑗,𝑘   0 ,𝑗,𝑘
Allowed substitution hints:   𝑉(𝑗,𝑘)   𝑊(𝑗,𝑘)

Proof of Theorem gsum2dlem2
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsum2d.w . . . 4 (𝜑𝐹 finSupp 0 )
21fsuppimpd 8818 . . 3 (𝜑 → (𝐹 supp 0 ) ∈ Fin)
3 dmfi 8780 . . 3 ((𝐹 supp 0 ) ∈ Fin → dom (𝐹 supp 0 ) ∈ Fin)
42, 3syl 17 . 2 (𝜑 → dom (𝐹 supp 0 ) ∈ Fin)
5 reseq2 5824 . . . . . . . . 9 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ↾ ∅))
6 res0 5833 . . . . . . . . 9 (𝐴 ↾ ∅) = ∅
75, 6syl6eq 2871 . . . . . . . 8 (𝑥 = ∅ → (𝐴𝑥) = ∅)
87reseq2d 5829 . . . . . . 7 (𝑥 = ∅ → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ ∅))
9 res0 5833 . . . . . . 7 (𝐹 ↾ ∅) = ∅
108, 9syl6eq 2871 . . . . . 6 (𝑥 = ∅ → (𝐹 ↾ (𝐴𝑥)) = ∅)
1110oveq2d 7149 . . . . 5 (𝑥 = ∅ → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg ∅))
12 mpteq1 5130 . . . . . . 7 (𝑥 = ∅ → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
13 mpt0 6466 . . . . . . 7 (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅
1412, 13syl6eq 2871 . . . . . 6 (𝑥 = ∅ → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅)
1514oveq2d 7149 . . . . 5 (𝑥 = ∅ → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg ∅))
1611, 15eqeq12d 2836 . . . 4 (𝑥 = ∅ → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg ∅) = (𝐺 Σg ∅)))
1716imbi2d 343 . . 3 (𝑥 = ∅ → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg ∅) = (𝐺 Σg ∅))))
18 reseq2 5824 . . . . . . 7 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
1918reseq2d 5829 . . . . . 6 (𝑥 = 𝑦 → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ (𝐴𝑦)))
2019oveq2d 7149 . . . . 5 (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴𝑦))))
21 mpteq1 5130 . . . . . 6 (𝑥 = 𝑦 → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
2221oveq2d 7149 . . . . 5 (𝑥 = 𝑦 → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
2320, 22eqeq12d 2836 . . . 4 (𝑥 = 𝑦 → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
2423imbi2d 343 . . 3 (𝑥 = 𝑦 → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
25 reseq2 5824 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴𝑥) = (𝐴 ↾ (𝑦 ∪ {𝑧})))
2625reseq2d 5829 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
2726oveq2d 7149 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))))
28 mpteq1 5130 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
2928oveq2d 7149 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
3027, 29eqeq12d 2836 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
3130imbi2d 343 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
32 reseq2 5824 . . . . . . 7 (𝑥 = dom (𝐹 supp 0 ) → (𝐴𝑥) = (𝐴 ↾ dom (𝐹 supp 0 )))
3332reseq2d 5829 . . . . . 6 (𝑥 = dom (𝐹 supp 0 ) → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 ))))
3433oveq2d 7149 . . . . 5 (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))))
35 mpteq1 5130 . . . . . 6 (𝑥 = dom (𝐹 supp 0 ) → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
3635oveq2d 7149 . . . . 5 (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
3734, 36eqeq12d 2836 . . . 4 (𝑥 = dom (𝐹 supp 0 ) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
3837imbi2d 343 . . 3 (𝑥 = dom (𝐹 supp 0 ) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
39 eqidd 2821 . . 3 (𝜑 → (𝐺 Σg ∅) = (𝐺 Σg ∅))
40 oveq1 7140 . . . . . 6 ((𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
41 gsum2d.b . . . . . . . . 9 𝐵 = (Base‘𝐺)
42 gsum2d.z . . . . . . . . 9 0 = (0g𝐺)
43 eqid 2820 . . . . . . . . 9 (+g𝐺) = (+g𝐺)
44 gsum2d.g . . . . . . . . . 10 (𝜑𝐺 ∈ CMnd)
4544adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐺 ∈ CMnd)
46 gsum2d.a . . . . . . . . . . 11 (𝜑𝐴𝑉)
47 resexg 5874 . . . . . . . . . . 11 (𝐴𝑉 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V)
4846, 47syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V)
4948adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V)
50 gsum2d.f . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
51 resss 5854 . . . . . . . . . . 11 (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴
52 fssres 6520 . . . . . . . . . . 11 ((𝐹:𝐴𝐵 ∧ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
5350, 51, 52sylancl 588 . . . . . . . . . 10 (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
5453adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
5550ffund 6494 . . . . . . . . . . . 12 (𝜑 → Fun 𝐹)
56 funres 6373 . . . . . . . . . . . 12 (Fun 𝐹 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
5755, 56syl 17 . . . . . . . . . . 11 (𝜑 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
5857adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
592adantr 483 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐹 supp 0 ) ∈ Fin)
60 fex 6965 . . . . . . . . . . . . . 14 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
6150, 46, 60syl2anc 586 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ V)
6242fvexi 6660 . . . . . . . . . . . . 13 0 ∈ V
63 ressuppss 7827 . . . . . . . . . . . . 13 ((𝐹 ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 ))
6461, 62, 63sylancl 588 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 ))
6564adantr 483 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 ))
6659, 65ssfid 8719 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)
67 resexg 5874 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V)
6861, 67syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V)
69 isfsupp 8815 . . . . . . . . . . . 12 (((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)))
7068, 62, 69sylancl 588 . . . . . . . . . . 11 (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)))
7170adantr 483 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)))
7258, 66, 71mpbir2and 711 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 )
73 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ¬ 𝑧𝑦)
74 disjsn 4623 . . . . . . . . . . . 12 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
7573, 74sylibr 236 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
7675reseq2d 5829 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴 ↾ (𝑦 ∩ {𝑧})) = (𝐴 ↾ ∅))
77 resindi 5845 . . . . . . . . . 10 (𝐴 ↾ (𝑦 ∩ {𝑧})) = ((𝐴𝑦) ∩ (𝐴 ↾ {𝑧}))
7876, 77, 63eqtr3g 2878 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐴𝑦) ∩ (𝐴 ↾ {𝑧})) = ∅)
79 resundi 5843 . . . . . . . . . 10 (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ (𝐴 ↾ {𝑧}))
8079a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ (𝐴 ↾ {𝑧})))
8141, 42, 43, 45, 49, 54, 72, 78, 80gsumsplit 19027 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))))
82 ssun1 4127 . . . . . . . . . . 11 𝑦 ⊆ (𝑦 ∪ {𝑧})
83 ssres2 5857 . . . . . . . . . . 11 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (𝐴𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})))
84 resabs1 5859 . . . . . . . . . . 11 ((𝐴𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)) = (𝐹 ↾ (𝐴𝑦)))
8582, 83, 84mp2b 10 . . . . . . . . . 10 ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)) = (𝐹 ↾ (𝐴𝑦))
8685oveq2i 7144 . . . . . . . . 9 (𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦))) = (𝐺 Σg (𝐹 ↾ (𝐴𝑦)))
87 ssun2 4128 . . . . . . . . . . 11 {𝑧} ⊆ (𝑦 ∪ {𝑧})
88 ssres2 5857 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})))
89 resabs1 5859 . . . . . . . . . . 11 ((𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧})))
9087, 88, 89mp2b 10 . . . . . . . . . 10 ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))
9190oveq2i 7144 . . . . . . . . 9 (𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))
9286, 91oveq12i 7145 . . . . . . . 8 ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
9381, 92syl6eq 2871 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
94 simprl 769 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑦 ∈ Fin)
95 gsum2d.r . . . . . . . . . . 11 (𝜑 → Rel 𝐴)
96 gsum2d.d . . . . . . . . . . 11 (𝜑𝐷𝑊)
97 gsum2d.s . . . . . . . . . . 11 (𝜑 → dom 𝐴𝐷)
9841, 42, 44, 46, 95, 96, 97, 50, 1gsum2dlem1 19069 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
9998ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑗𝑦) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
100 vex 3476 . . . . . . . . . 10 𝑧 ∈ V
101100a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑧 ∈ V)
102 sneq 4553 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧 → {𝑗} = {𝑧})
103102imaeq2d 5905 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝐴 “ {𝑗}) = (𝐴 “ {𝑧}))
104 oveq1 7140 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑗𝐹𝑘) = (𝑧𝐹𝑘))
105103, 104mpteq12dv 5127 . . . . . . . . . . . . . 14 (𝑗 = 𝑧 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))
106105oveq2d 7149 . . . . . . . . . . . . 13 (𝑗 = 𝑧 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))))
107106eleq1d 2895 . . . . . . . . . . . 12 (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵 ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵))
108107imbi2d 343 . . . . . . . . . . 11 (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)))
109108, 98chvarvv 2005 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)
110109adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)
11141, 43, 45, 94, 99, 101, 73, 110, 106gsumunsn 19059 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))))
112102reseq2d 5829 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝐴 ↾ {𝑗}) = (𝐴 ↾ {𝑧}))
113112reseq2d 5829 . . . . . . . . . . . . . 14 (𝑗 = 𝑧 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝐹 ↾ (𝐴 ↾ {𝑧})))
114113oveq2d 7149 . . . . . . . . . . . . 13 (𝑗 = 𝑧 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
115106, 114eqeq12d 2836 . . . . . . . . . . . 12 (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
116115imbi2d 343 . . . . . . . . . . 11 (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗})))) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))))
117 imaexg 7598 . . . . . . . . . . . . . 14 (𝐴𝑉 → (𝐴 “ {𝑗}) ∈ V)
11846, 117syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐴 “ {𝑗}) ∈ V)
119 vex 3476 . . . . . . . . . . . . . . . 16 𝑗 ∈ V
120 vex 3476 . . . . . . . . . . . . . . . 16 𝑘 ∈ V
121119, 120elimasn 5930 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐴 “ {𝑗}) ↔ ⟨𝑗, 𝑘⟩ ∈ 𝐴)
122 df-ov 7136 . . . . . . . . . . . . . . . 16 (𝑗𝐹𝑘) = (𝐹‘⟨𝑗, 𝑘⟩)
12350ffvelrnda 6827 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ 𝐴) → (𝐹‘⟨𝑗, 𝑘⟩) ∈ 𝐵)
124122, 123eqeltrid 2915 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ 𝐴) → (𝑗𝐹𝑘) ∈ 𝐵)
125121, 124sylan2b 595 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) ∈ 𝐵)
126125fmpttd 6855 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)):(𝐴 “ {𝑗})⟶𝐵)
127 funmpt 6369 . . . . . . . . . . . . . . 15 Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))
128127a1i 11 . . . . . . . . . . . . . 14 (𝜑 → Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))
129 rnfi 8785 . . . . . . . . . . . . . . . 16 ((𝐹 supp 0 ) ∈ Fin → ran (𝐹 supp 0 ) ∈ Fin)
1302, 129syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ran (𝐹 supp 0 ) ∈ Fin)
131121biimpi 218 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐴 “ {𝑗}) → ⟨𝑗, 𝑘⟩ ∈ 𝐴)
132119, 120opelrn 5789 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 ) → 𝑘 ∈ ran (𝐹 supp 0 ))
133132con3i 157 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ ran (𝐹 supp 0 ) → ¬ ⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 ))
134131, 133anim12i 614 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 )) → (⟨𝑗, 𝑘⟩ ∈ 𝐴 ∧ ¬ ⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 )))
135 eldif 3923 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) ↔ (𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 )))
136 eldif 3923 . . . . . . . . . . . . . . . . . 18 (⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )) ↔ (⟨𝑗, 𝑘⟩ ∈ 𝐴 ∧ ¬ ⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 )))
137134, 135, 1363imtr4i 294 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) → ⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
138 ssidd 3969 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
13962a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑0 ∈ V)
14050, 138, 46, 139suppssr 7839 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘⟨𝑗, 𝑘⟩) = 0 )
141122, 140syl5eq 2867 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 )
142137, 141sylan2 594 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 )
143142, 118suppss2 7842 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ⊆ ran (𝐹 supp 0 ))
144130, 143ssfid 8719 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈ Fin)
145118mptexd 6963 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V)
146 isfsupp 8815 . . . . . . . . . . . . . . 15 (((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V ∧ 0 ∈ V) → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈ Fin)))
147145, 62, 146sylancl 588 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈ Fin)))
148128, 144, 147mpbir2and 711 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 )
149 2ndconst 7774 . . . . . . . . . . . . . 14 (𝑗 ∈ V → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗}))
150119, 149mp1i 13 . . . . . . . . . . . . 13 (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗}))
15141, 42, 44, 118, 126, 148, 150gsumf1o 19015 . . . . . . . . . . . 12 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
152 1st2nd2 7706 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
153 xp1st 7699 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st𝑥) ∈ {𝑗})
154 elsni 4560 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ {𝑗} → (1st𝑥) = 𝑗)
155153, 154syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st𝑥) = 𝑗)
156155opeq1d 4785 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨𝑗, (2nd𝑥)⟩)
157152, 156eqtrd 2855 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = ⟨𝑗, (2nd𝑥)⟩)
158157fveq2d 6650 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹𝑥) = (𝐹‘⟨𝑗, (2nd𝑥)⟩))
159 df-ov 7136 . . . . . . . . . . . . . . . 16 (𝑗𝐹(2nd𝑥)) = (𝐹‘⟨𝑗, (2nd𝑥)⟩)
160158, 159syl6eqr 2873 . . . . . . . . . . . . . . 15 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹𝑥) = (𝑗𝐹(2nd𝑥)))
161160mpteq2ia 5133 . . . . . . . . . . . . . 14 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd𝑥)))
16250feqmptd 6709 . . . . . . . . . . . . . . . 16 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
163162reseq1d 5828 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})))
164 resss 5854 . . . . . . . . . . . . . . . . 17 (𝐴 ↾ {𝑗}) ⊆ 𝐴
165 resmpt 5881 . . . . . . . . . . . . . . . . 17 ((𝐴 ↾ {𝑗}) ⊆ 𝐴 → ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹𝑥)))
166164, 165ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹𝑥))
167 ressn 6112 . . . . . . . . . . . . . . . . 17 (𝐴 ↾ {𝑗}) = ({𝑗} × (𝐴 “ {𝑗}))
168167mpteq1i 5132 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥))
169166, 168eqtri 2843 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥))
170163, 169syl6eq 2871 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥)))
171 xp2nd 7700 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (2nd𝑥) ∈ (𝐴 “ {𝑗}))
172171adantl 484 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗}))) → (2nd𝑥) ∈ (𝐴 “ {𝑗}))
173 fo2nd 7688 . . . . . . . . . . . . . . . . . . 19 2nd :V–onto→V
174 fof 6566 . . . . . . . . . . . . . . . . . . 19 (2nd :V–onto→V → 2nd :V⟶V)
175173, 174mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2nd :V⟶V)
176175feqmptd 6709 . . . . . . . . . . . . . . . . 17 (𝜑 → 2nd = (𝑥 ∈ V ↦ (2nd𝑥)))
177176reseq1d 5828 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))) = ((𝑥 ∈ V ↦ (2nd𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))))
178 ssv 3970 . . . . . . . . . . . . . . . . 17 ({𝑗} × (𝐴 “ {𝑗})) ⊆ V
179 resmpt 5881 . . . . . . . . . . . . . . . . 17 (({𝑗} × (𝐴 “ {𝑗})) ⊆ V → ((𝑥 ∈ V ↦ (2nd𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd𝑥)))
180178, 179ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ↦ (2nd𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd𝑥))
181177, 180syl6eq 2871 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd𝑥)))
182 eqidd 2821 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))
183 oveq2 7141 . . . . . . . . . . . . . . 15 (𝑘 = (2nd𝑥) → (𝑗𝐹𝑘) = (𝑗𝐹(2nd𝑥)))
184172, 181, 182, 183fmptco 6867 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd𝑥))))
185161, 170, 1843eqtr4a 2881 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))
186185oveq2d 7149 . . . . . . . . . . . 12 (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
187151, 186eqtr4d 2858 . . . . . . . . . . 11 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))))
188116, 187chvarvv 2005 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
189188adantr 483 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
190189oveq2d 7149 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
191111, 190eqtrd 2855 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
19293, 191eqeq12d 2836 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))))
19340, 192syl5ibr 248 . . . . 5 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
194193expcom 416 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
195194a2d 29 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
19617, 24, 31, 38, 39, 195findcard2s 8737 . 2 (dom (𝐹 supp 0 ) ∈ Fin → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
1974, 196mpcom 38 1 (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398   = wceq 1537  wcel 2114  Vcvv 3473  cdif 3910  cun 3911  cin 3912  wss 3913  c0 4269  {csn 4543  cop 4549   class class class wbr 5042  cmpt 5122   × cxp 5529  dom cdm 5531  ran crn 5532  cres 5533  cima 5534  ccom 5535  Rel wrel 5536  Fun wfun 6325  wf 6327  ontowfo 6329  1-1-ontowf1o 6330  cfv 6331  (class class class)co 7133  1st c1st 7665  2nd c2nd 7666   supp csupp 7808  Fincfn 8487   finSupp cfsupp 8811  Basecbs 16462  +gcplusg 16544  0gc0g 16692   Σg cgsu 16693  CMndccmn 18885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-iin 4898  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-of 7387  df-om 7559  df-1st 7667  df-2nd 7668  df-supp 7809  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-fsupp 8812  df-oi 8952  df-card 9346  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-nn 11617  df-2 11679  df-n0 11877  df-z 11961  df-uz 12223  df-fz 12877  df-fzo 13018  df-seq 13354  df-hash 13676  df-ndx 16465  df-slot 16466  df-base 16468  df-sets 16469  df-ress 16470  df-plusg 16557  df-0g 16694  df-gsum 16695  df-mre 16836  df-mrc 16837  df-acs 16839  df-mgm 17831  df-sgrp 17880  df-mnd 17891  df-submnd 17936  df-mulg 18204  df-cntz 18426  df-cmn 18887
This theorem is referenced by:  gsum2d  19071
  Copyright terms: Public domain W3C validator