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

Theorem gsum2dlem2 18756
 Description: Lemma for gsum2d 18757. (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 8570 . . 3 (𝜑 → (𝐹 supp 0 ) ∈ Fin)
3 dmfi 8532 . . 3 ((𝐹 supp 0 ) ∈ Fin → dom (𝐹 supp 0 ) ∈ Fin)
42, 3syl 17 . 2 (𝜑 → dom (𝐹 supp 0 ) ∈ Fin)
5 reseq2 5637 . . . . . . . . 9 (𝑥 = ∅ → (𝐴𝑥) = (𝐴 ↾ ∅))
6 res0 5646 . . . . . . . . 9 (𝐴 ↾ ∅) = ∅
75, 6syl6eq 2830 . . . . . . . 8 (𝑥 = ∅ → (𝐴𝑥) = ∅)
87reseq2d 5642 . . . . . . 7 (𝑥 = ∅ → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ ∅))
9 res0 5646 . . . . . . 7 (𝐹 ↾ ∅) = ∅
108, 9syl6eq 2830 . . . . . 6 (𝑥 = ∅ → (𝐹 ↾ (𝐴𝑥)) = ∅)
1110oveq2d 6938 . . . . 5 (𝑥 = ∅ → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg ∅))
12 mpteq1 4972 . . . . . . 7 (𝑥 = ∅ → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
13 mpt0 6267 . . . . . . 7 (𝑗 ∈ ∅ ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅
1412, 13syl6eq 2830 . . . . . 6 (𝑥 = ∅ → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = ∅)
1514oveq2d 6938 . . . . 5 (𝑥 = ∅ → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg ∅))
1611, 15eqeq12d 2793 . . . 4 (𝑥 = ∅ → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg ∅) = (𝐺 Σg ∅)))
1716imbi2d 332 . . 3 (𝑥 = ∅ → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg ∅) = (𝐺 Σg ∅))))
18 reseq2 5637 . . . . . . 7 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
1918reseq2d 5642 . . . . . 6 (𝑥 = 𝑦 → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ (𝐴𝑦)))
2019oveq2d 6938 . . . . 5 (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴𝑦))))
21 mpteq1 4972 . . . . . 6 (𝑥 = 𝑦 → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
2221oveq2d 6938 . . . . 5 (𝑥 = 𝑦 → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
2320, 22eqeq12d 2793 . . . 4 (𝑥 = 𝑦 → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
2423imbi2d 332 . . 3 (𝑥 = 𝑦 → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
25 reseq2 5637 . . . . . . 7 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐴𝑥) = (𝐴 ↾ (𝑦 ∪ {𝑧})))
2625reseq2d 5642 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
2726oveq2d 6938 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))))
28 mpteq1 4972 . . . . . 6 (𝑥 = (𝑦 ∪ {𝑧}) → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
2928oveq2d 6938 . . . . 5 (𝑥 = (𝑦 ∪ {𝑧}) → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
3027, 29eqeq12d 2793 . . . 4 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
3130imbi2d 332 . . 3 (𝑥 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
32 reseq2 5637 . . . . . . 7 (𝑥 = dom (𝐹 supp 0 ) → (𝐴𝑥) = (𝐴 ↾ dom (𝐹 supp 0 )))
3332reseq2d 5642 . . . . . 6 (𝑥 = dom (𝐹 supp 0 ) → (𝐹 ↾ (𝐴𝑥)) = (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 ))))
3433oveq2d 6938 . . . . 5 (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))))
35 mpteq1 4972 . . . . . 6 (𝑥 = dom (𝐹 supp 0 ) → (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))) = (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))
3635oveq2d 6938 . . . . 5 (𝑥 = dom (𝐹 supp 0 ) → (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))
3734, 36eqeq12d 2793 . . . 4 (𝑥 = dom (𝐹 supp 0 ) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
3837imbi2d 332 . . 3 (𝑥 = dom (𝐹 supp 0 ) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑥))) = (𝐺 Σg (𝑗𝑥 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) ↔ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
39 eqidd 2779 . . 3 (𝜑 → (𝐺 Σg ∅) = (𝐺 Σg ∅))
40 oveq1 6929 . . . . . 6 ((𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
41 gsum2d.b . . . . . . . . 9 𝐵 = (Base‘𝐺)
42 gsum2d.z . . . . . . . . 9 0 = (0g𝐺)
43 eqid 2778 . . . . . . . . 9 (+g𝐺) = (+g𝐺)
44 gsum2d.g . . . . . . . . . 10 (𝜑𝐺 ∈ CMnd)
4544adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝐺 ∈ CMnd)
46 gsum2d.a . . . . . . . . . . 11 (𝜑𝐴𝑉)
47 resexg 5692 . . . . . . . . . . 11 (𝐴𝑉 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V)
4846, 47syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V)
4948adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) ∈ V)
50 gsum2d.f . . . . . . . . . . 11 (𝜑𝐹:𝐴𝐵)
51 resss 5671 . . . . . . . . . . 11 (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴
52 fssres 6320 . . . . . . . . . . 11 ((𝐹:𝐴𝐵 ∧ (𝐴 ↾ (𝑦 ∪ {𝑧})) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
5350, 51, 52sylancl 580 . . . . . . . . . 10 (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
5453adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))):(𝐴 ↾ (𝑦 ∪ {𝑧}))⟶𝐵)
5550ffund 6295 . . . . . . . . . . . 12 (𝜑 → Fun 𝐹)
56 funres 6177 . . . . . . . . . . . 12 (Fun 𝐹 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
5755, 56syl 17 . . . . . . . . . . 11 (𝜑 → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
5857adantr 474 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))))
592adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐹 supp 0 ) ∈ Fin)
60 fex 6761 . . . . . . . . . . . . . 14 ((𝐹:𝐴𝐵𝐴𝑉) → 𝐹 ∈ V)
6150, 46, 60syl2anc 579 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ V)
6242fvexi 6460 . . . . . . . . . . . . 13 0 ∈ V
63 ressuppss 7595 . . . . . . . . . . . . 13 ((𝐹 ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 ))
6461, 62, 63sylancl 580 . . . . . . . . . . . 12 (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 ))
6564adantr 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ⊆ (𝐹 supp 0 ))
6659, 65ssfid 8471 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)
67 resexg 5692 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V)
6861, 67syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V)
69 isfsupp 8567 . . . . . . . . . . . 12 (((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∈ V ∧ 0 ∈ V) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)))
7068, 62, 69sylancl 580 . . . . . . . . . . 11 (𝜑 → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)))
7170adantr 474 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 ↔ (Fun (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ∧ ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) supp 0 ) ∈ Fin)))
7258, 66, 71mpbir2and 703 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) finSupp 0 )
73 simprr 763 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ¬ 𝑧𝑦)
74 disjsn 4478 . . . . . . . . . . . 12 ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝑦)
7573, 74sylibr 226 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝑦 ∩ {𝑧}) = ∅)
7675reseq2d 5642 . . . . . . . . . 10 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴 ↾ (𝑦 ∩ {𝑧})) = (𝐴 ↾ ∅))
77 resindi 5662 . . . . . . . . . 10 (𝐴 ↾ (𝑦 ∩ {𝑧})) = ((𝐴𝑦) ∩ (𝐴 ↾ {𝑧}))
7876, 77, 63eqtr3g 2837 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐴𝑦) ∩ (𝐴 ↾ {𝑧})) = ∅)
79 resundi 5660 . . . . . . . . . 10 (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ (𝐴 ↾ {𝑧}))
8079a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐴 ↾ (𝑦 ∪ {𝑧})) = ((𝐴𝑦) ∪ (𝐴 ↾ {𝑧})))
8141, 42, 43, 45, 49, 54, 72, 78, 80gsumsplit 18714 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))))
82 ssun1 3999 . . . . . . . . . . 11 𝑦 ⊆ (𝑦 ∪ {𝑧})
83 ssres2 5674 . . . . . . . . . . 11 (𝑦 ⊆ (𝑦 ∪ {𝑧}) → (𝐴𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})))
84 resabs1 5676 . . . . . . . . . . 11 ((𝐴𝑦) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)) = (𝐹 ↾ (𝐴𝑦)))
8582, 83, 84mp2b 10 . . . . . . . . . 10 ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)) = (𝐹 ↾ (𝐴𝑦))
8685oveq2i 6933 . . . . . . . . 9 (𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦))) = (𝐺 Σg (𝐹 ↾ (𝐴𝑦)))
87 ssun2 4000 . . . . . . . . . . 11 {𝑧} ⊆ (𝑦 ∪ {𝑧})
88 ssres2 5674 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑦 ∪ {𝑧}) → (𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})))
89 resabs1 5676 . . . . . . . . . . 11 ((𝐴 ↾ {𝑧}) ⊆ (𝐴 ↾ (𝑦 ∪ {𝑧})) → ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧})))
9087, 88, 89mp2b 10 . . . . . . . . . 10 ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})) = (𝐹 ↾ (𝐴 ↾ {𝑧}))
9190oveq2i 6933 . . . . . . . . 9 (𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))
9286, 91oveq12i 6934 . . . . . . . 8 ((𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg ((𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧}))) ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
9381, 92syl6eq 2830 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
94 simprl 761 . . . . . . . . 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 18755 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
9998ad2antrr 716 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) ∧ 𝑗𝑦) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵)
100 vex 3401 . . . . . . . . . 10 𝑧 ∈ V
101100a1i 11 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → 𝑧 ∈ V)
102 sneq 4408 . . . . . . . . . . . . . . . 16 (𝑗 = 𝑧 → {𝑗} = {𝑧})
103102imaeq2d 5720 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝐴 “ {𝑗}) = (𝐴 “ {𝑧}))
104 oveq1 6929 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝑗𝐹𝑘) = (𝑧𝐹𝑘))
105103, 104mpteq12dv 4969 . . . . . . . . . . . . . 14 (𝑗 = 𝑧 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))
106105oveq2d 6938 . . . . . . . . . . . . 13 (𝑗 = 𝑧 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))))
107106eleq1d 2844 . . . . . . . . . . . 12 (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵 ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵))
108107imbi2d 332 . . . . . . . . . . 11 (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)))
109108, 98chvarv 2361 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)
110109adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) ∈ 𝐵)
11141, 43, 45, 94, 99, 101, 73, 110, 106gsumunsn 18745 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))))
112102reseq2d 5642 . . . . . . . . . . . . . . 15 (𝑗 = 𝑧 → (𝐴 ↾ {𝑗}) = (𝐴 ↾ {𝑧}))
113112reseq2d 5642 . . . . . . . . . . . . . 14 (𝑗 = 𝑧 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝐹 ↾ (𝐴 ↾ {𝑧})))
114113oveq2d 6938 . . . . . . . . . . . . 13 (𝑗 = 𝑧 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
115106, 114eqeq12d 2793 . . . . . . . . . . . 12 (𝑗 = 𝑧 → ((𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) ↔ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
116115imbi2d 332 . . . . . . . . . . 11 (𝑗 = 𝑧 → ((𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗})))) ↔ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))))
117 imaexg 7382 . . . . . . . . . . . . . 14 (𝐴𝑉 → (𝐴 “ {𝑗}) ∈ V)
11846, 117syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝐴 “ {𝑗}) ∈ V)
119 vex 3401 . . . . . . . . . . . . . . . 16 𝑗 ∈ V
120 vex 3401 . . . . . . . . . . . . . . . 16 𝑘 ∈ V
121119, 120elimasn 5744 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐴 “ {𝑗}) ↔ ⟨𝑗, 𝑘⟩ ∈ 𝐴)
122 df-ov 6925 . . . . . . . . . . . . . . . 16 (𝑗𝐹𝑘) = (𝐹‘⟨𝑗, 𝑘⟩)
12350ffvelrnda 6623 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ 𝐴) → (𝐹‘⟨𝑗, 𝑘⟩) ∈ 𝐵)
124122, 123syl5eqel 2863 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ 𝐴) → (𝑗𝐹𝑘) ∈ 𝐵)
125121, 124sylan2b 587 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐴 “ {𝑗})) → (𝑗𝐹𝑘) ∈ 𝐵)
126125fmpttd 6649 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)):(𝐴 “ {𝑗})⟶𝐵)
127 funmpt 6173 . . . . . . . . . . . . . . 15 Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))
128127a1i 11 . . . . . . . . . . . . . 14 (𝜑 → Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))
129 rnfi 8537 . . . . . . . . . . . . . . . 16 ((𝐹 supp 0 ) ∈ Fin → ran (𝐹 supp 0 ) ∈ Fin)
1302, 129syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ran (𝐹 supp 0 ) ∈ Fin)
131121biimpi 208 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐴 “ {𝑗}) → ⟨𝑗, 𝑘⟩ ∈ 𝐴)
132119, 120opelrn 5603 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 ) → 𝑘 ∈ ran (𝐹 supp 0 ))
133132con3i 152 . . . . . . . . . . . . . . . . . . 19 𝑘 ∈ ran (𝐹 supp 0 ) → ¬ ⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 ))
134131, 133anim12i 606 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 )) → (⟨𝑗, 𝑘⟩ ∈ 𝐴 ∧ ¬ ⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 )))
135 eldif 3802 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) ↔ (𝑘 ∈ (𝐴 “ {𝑗}) ∧ ¬ 𝑘 ∈ ran (𝐹 supp 0 )))
136 eldif 3802 . . . . . . . . . . . . . . . . . 18 (⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )) ↔ (⟨𝑗, 𝑘⟩ ∈ 𝐴 ∧ ¬ ⟨𝑗, 𝑘⟩ ∈ (𝐹 supp 0 )))
137134, 135, 1363imtr4i 284 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 )) → ⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 )))
138 ssidd 3843 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 supp 0 ) ⊆ (𝐹 supp 0 ))
13962a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑0 ∈ V)
14050, 138, 46, 139suppssr 7608 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝐹‘⟨𝑗, 𝑘⟩) = 0 )
141122, 140syl5eq 2826 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ⟨𝑗, 𝑘⟩ ∈ (𝐴 ∖ (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 )
142137, 141sylan2 586 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ ((𝐴 “ {𝑗}) ∖ ran (𝐹 supp 0 ))) → (𝑗𝐹𝑘) = 0 )
143142, 118suppss2 7611 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ⊆ ran (𝐹 supp 0 ))
144130, 143ssfid 8471 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈ Fin)
145118mptexd 6759 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V)
146 isfsupp 8567 . . . . . . . . . . . . . . 15 (((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∈ V ∧ 0 ∈ V) → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈ Fin)))
147145, 62, 146sylancl 580 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 ↔ (Fun (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∧ ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) supp 0 ) ∈ Fin)))
148128, 144, 147mpbir2and 703 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) finSupp 0 )
149 2ndconst 7547 . . . . . . . . . . . . . 14 (𝑗 ∈ V → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗}))
150119, 149mp1i 13 . . . . . . . . . . . . 13 (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))):({𝑗} × (𝐴 “ {𝑗}))–1-1-onto→(𝐴 “ {𝑗}))
15141, 42, 44, 118, 126, 148, 150gsumf1o 18703 . . . . . . . . . . . 12 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
152 1st2nd2 7484 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
153 xp1st 7477 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st𝑥) ∈ {𝑗})
154 elsni 4415 . . . . . . . . . . . . . . . . . . . 20 ((1st𝑥) ∈ {𝑗} → (1st𝑥) = 𝑗)
155153, 154syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (1st𝑥) = 𝑗)
156155opeq1d 4642 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → ⟨(1st𝑥), (2nd𝑥)⟩ = ⟨𝑗, (2nd𝑥)⟩)
157152, 156eqtrd 2814 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → 𝑥 = ⟨𝑗, (2nd𝑥)⟩)
158157fveq2d 6450 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹𝑥) = (𝐹‘⟨𝑗, (2nd𝑥)⟩))
159 df-ov 6925 . . . . . . . . . . . . . . . 16 (𝑗𝐹(2nd𝑥)) = (𝐹‘⟨𝑗, (2nd𝑥)⟩)
160158, 159syl6eqr 2832 . . . . . . . . . . . . . . 15 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (𝐹𝑥) = (𝑗𝐹(2nd𝑥)))
161160mpteq2ia 4975 . . . . . . . . . . . . . 14 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd𝑥)))
16250feqmptd 6509 . . . . . . . . . . . . . . . 16 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
163162reseq1d 5641 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})))
164 resss 5671 . . . . . . . . . . . . . . . . 17 (𝐴 ↾ {𝑗}) ⊆ 𝐴
165 resmpt 5699 . . . . . . . . . . . . . . . . 17 ((𝐴 ↾ {𝑗}) ⊆ 𝐴 → ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹𝑥)))
166164, 165ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹𝑥))
167 ressn 5925 . . . . . . . . . . . . . . . . 17 (𝐴 ↾ {𝑗}) = ({𝑗} × (𝐴 “ {𝑗}))
168167mpteq1i 4974 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴 ↾ {𝑗}) ↦ (𝐹𝑥)) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥))
169166, 168eqtri 2802 . . . . . . . . . . . . . . 15 ((𝑥𝐴 ↦ (𝐹𝑥)) ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥))
170163, 169syl6eq 2830 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝐹𝑥)))
171 xp2nd 7478 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) → (2nd𝑥) ∈ (𝐴 “ {𝑗}))
172171adantl 475 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗}))) → (2nd𝑥) ∈ (𝐴 “ {𝑗}))
173 fo2nd 7466 . . . . . . . . . . . . . . . . . . 19 2nd :V–onto→V
174 fof 6366 . . . . . . . . . . . . . . . . . . 19 (2nd :V–onto→V → 2nd :V⟶V)
175173, 174mp1i 13 . . . . . . . . . . . . . . . . . 18 (𝜑 → 2nd :V⟶V)
176175feqmptd 6509 . . . . . . . . . . . . . . . . 17 (𝜑 → 2nd = (𝑥 ∈ V ↦ (2nd𝑥)))
177176reseq1d 5641 . . . . . . . . . . . . . . . 16 (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))) = ((𝑥 ∈ V ↦ (2nd𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))))
178 ssv 3844 . . . . . . . . . . . . . . . . 17 ({𝑗} × (𝐴 “ {𝑗})) ⊆ V
179 resmpt 5699 . . . . . . . . . . . . . . . . 17 (({𝑗} × (𝐴 “ {𝑗})) ⊆ V → ((𝑥 ∈ V ↦ (2nd𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd𝑥)))
180178, 179ax-mp 5 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ V ↦ (2nd𝑥)) ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd𝑥))
181177, 180syl6eq 2830 . . . . . . . . . . . . . . 15 (𝜑 → (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (2nd𝑥)))
182 eqidd 2779 . . . . . . . . . . . . . . 15 (𝜑 → (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) = (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))
183 oveq2 6930 . . . . . . . . . . . . . . 15 (𝑘 = (2nd𝑥) → (𝑗𝐹𝑘) = (𝑗𝐹(2nd𝑥)))
184172, 181, 182, 183fmptco 6661 . . . . . . . . . . . . . 14 (𝜑 → ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))) = (𝑥 ∈ ({𝑗} × (𝐴 “ {𝑗})) ↦ (𝑗𝐹(2nd𝑥))))
185161, 170, 1843eqtr4a 2840 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ↾ (𝐴 ↾ {𝑗})) = ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗})))))
186185oveq2d 6938 . . . . . . . . . . . 12 (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))) = (𝐺 Σg ((𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)) ∘ (2nd ↾ ({𝑗} × (𝐴 “ {𝑗}))))))
187151, 186eqtr4d 2817 . . . . . . . . . . 11 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑗}))))
188116, 187chvarv 2361 . . . . . . . . . 10 (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
189188adantr 474 . . . . . . . . 9 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘))) = (𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))
190189oveq2d 6938 . . . . . . . 8 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑧}) ↦ (𝑧𝐹𝑘)))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
191111, 190eqtrd 2814 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))))
19293, 191eqeq12d 2793 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) ↔ ((𝐺 Σg (𝐹 ↾ (𝐴𝑦)))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧})))) = ((𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))(+g𝐺)(𝐺 Σg (𝐹 ↾ (𝐴 ↾ {𝑧}))))))
19340, 192syl5ibr 238 . . . . 5 ((𝜑 ∧ (𝑦 ∈ Fin ∧ ¬ 𝑧𝑦)) → ((𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))))
194193expcom 404 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜑 → ((𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))) → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
195194a2d 29 . . 3 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → ((𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴𝑦))) = (𝐺 Σg (𝑗𝑦 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) → (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ (𝑦 ∪ {𝑧})))) = (𝐺 Σg (𝑗 ∈ (𝑦 ∪ {𝑧}) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))))))))
19617, 24, 31, 38, 39, 195findcard2s 8489 . 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 198   ∧ wa 386   = wceq 1601   ∈ wcel 2107  Vcvv 3398   ∖ cdif 3789   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  {csn 4398  ⟨cop 4404   class class class wbr 4886   ↦ cmpt 4965   × cxp 5353  dom cdm 5355  ran crn 5356   ↾ cres 5357   “ cima 5358   ∘ ccom 5359  Rel wrel 5360  Fun wfun 6129  ⟶wf 6131  –onto→wfo 6133  –1-1-onto→wf1o 6134  ‘cfv 6135  (class class class)co 6922  1st c1st 7443  2nd c2nd 7444   supp csupp 7576  Fincfn 8241   finSupp cfsupp 8563  Basecbs 16255  +gcplusg 16338  0gc0g 16486   Σg cgsu 16487  CMndccmn 18579 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-oi 8704  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-2 11438  df-n0 11643  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-seq 13120  df-hash 13436  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-0g 16488  df-gsum 16489  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581 This theorem is referenced by:  gsum2d  18757
 Copyright terms: Public domain W3C validator