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

Theorem gsumpart 32814
Description: Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024.)
Hypotheses
Ref Expression
gsumpart.b 𝐵 = (Base‘𝐺)
gsumpart.z 0 = (0g𝐺)
gsumpart.g (𝜑𝐺 ∈ CMnd)
gsumpart.a (𝜑𝐴𝑉)
gsumpart.x (𝜑𝑋𝑊)
gsumpart.f (𝜑𝐹:𝐴𝐵)
gsumpart.w (𝜑𝐹 finSupp 0 )
gsumpart.1 (𝜑Disj 𝑥𝑋 𝐶)
gsumpart.2 (𝜑 𝑥𝑋 𝐶 = 𝐴)
Assertion
Ref Expression
gsumpart (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝑋 ↦ (𝐺 Σg (𝐹𝐶)))))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺   𝑥,𝑋   𝜑,𝑥
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)   𝑊(𝑥)   0 (𝑥)

Proof of Theorem gsumpart
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 gsumpart.b . . 3 𝐵 = (Base‘𝐺)
2 gsumpart.z . . 3 0 = (0g𝐺)
3 gsumpart.g . . 3 (𝜑𝐺 ∈ CMnd)
4 gsumpart.a . . 3 (𝜑𝐴𝑉)
5 gsumpart.f . . 3 (𝜑𝐹:𝐴𝐵)
6 gsumpart.w . . 3 (𝜑𝐹 finSupp 0 )
7 eqid 2725 . . . 4 𝑥𝑋 ({𝑥} × 𝐶) = 𝑥𝑋 ({𝑥} × 𝐶)
8 gsumpart.x . . . 4 (𝜑𝑋𝑊)
9 gsumpart.1 . . . 4 (𝜑Disj 𝑥𝑋 𝐶)
10 gsumpart.2 . . . 4 (𝜑 𝑥𝑋 𝐶 = 𝐴)
117, 4, 8, 9, 102ndresdjuf1o 32481 . . 3 (𝜑 → (2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)–1-1-onto𝐴)
121, 2, 3, 4, 5, 6, 11gsumf1o 19875 . 2 (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))))
13 vsnex 5425 . . . . . . 7 {𝑥} ∈ V
1413a1i 11 . . . . . 6 ((𝜑𝑥𝑋) → {𝑥} ∈ V)
154adantr 479 . . . . . . 7 ((𝜑𝑥𝑋) → 𝐴𝑉)
16 ssidd 3996 . . . . . . . . . 10 (𝜑𝐴𝐴)
1710, 16eqsstrd 4011 . . . . . . . . 9 (𝜑 𝑥𝑋 𝐶𝐴)
18 iunss 5043 . . . . . . . . 9 ( 𝑥𝑋 𝐶𝐴 ↔ ∀𝑥𝑋 𝐶𝐴)
1917, 18sylib 217 . . . . . . . 8 (𝜑 → ∀𝑥𝑋 𝐶𝐴)
2019r19.21bi 3239 . . . . . . 7 ((𝜑𝑥𝑋) → 𝐶𝐴)
2115, 20ssexd 5319 . . . . . 6 ((𝜑𝑥𝑋) → 𝐶 ∈ V)
2214, 21xpexd 7751 . . . . 5 ((𝜑𝑥𝑋) → ({𝑥} × 𝐶) ∈ V)
2322ralrimiva 3136 . . . 4 (𝜑 → ∀𝑥𝑋 ({𝑥} × 𝐶) ∈ V)
24 iunexg 7965 . . . 4 ((𝑋𝑊 ∧ ∀𝑥𝑋 ({𝑥} × 𝐶) ∈ V) → 𝑥𝑋 ({𝑥} × 𝐶) ∈ V)
258, 23, 24syl2anc 582 . . 3 (𝜑 𝑥𝑋 ({𝑥} × 𝐶) ∈ V)
26 relxp 5690 . . . . . 6 Rel ({𝑥} × 𝐶)
2726a1i 11 . . . . 5 ((𝜑𝑥𝑋) → Rel ({𝑥} × 𝐶))
2827ralrimiva 3136 . . . 4 (𝜑 → ∀𝑥𝑋 Rel ({𝑥} × 𝐶))
29 reliun 5812 . . . 4 (Rel 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∀𝑥𝑋 Rel ({𝑥} × 𝐶))
3028, 29sylibr 233 . . 3 (𝜑 → Rel 𝑥𝑋 ({𝑥} × 𝐶))
31 dmiun 5910 . . . . . 6 dom 𝑥𝑋 ({𝑥} × 𝐶) = 𝑥𝑋 dom ({𝑥} × 𝐶)
32 dmxpss 6170 . . . . . . . 8 dom ({𝑥} × 𝐶) ⊆ {𝑥}
3332rgenw 3055 . . . . . . 7 𝑥𝑋 dom ({𝑥} × 𝐶) ⊆ {𝑥}
34 ss2iun 5009 . . . . . . 7 (∀𝑥𝑋 dom ({𝑥} × 𝐶) ⊆ {𝑥} → 𝑥𝑋 dom ({𝑥} × 𝐶) ⊆ 𝑥𝑋 {𝑥})
3533, 34ax-mp 5 . . . . . 6 𝑥𝑋 dom ({𝑥} × 𝐶) ⊆ 𝑥𝑋 {𝑥}
3631, 35eqsstri 4007 . . . . 5 dom 𝑥𝑋 ({𝑥} × 𝐶) ⊆ 𝑥𝑋 {𝑥}
37 iunid 5058 . . . . 5 𝑥𝑋 {𝑥} = 𝑋
3836, 37sseqtri 4009 . . . 4 dom 𝑥𝑋 ({𝑥} × 𝐶) ⊆ 𝑋
3938a1i 11 . . 3 (𝜑 → dom 𝑥𝑋 ({𝑥} × 𝐶) ⊆ 𝑋)
40 fo2nd 8012 . . . . . . . 8 2nd :V–onto→V
41 fof 6806 . . . . . . . 8 (2nd :V–onto→V → 2nd :V⟶V)
4240, 41ax-mp 5 . . . . . . 7 2nd :V⟶V
43 ssv 3997 . . . . . . 7 𝑥𝑋 ({𝑥} × 𝐶) ⊆ V
44 fssres 6758 . . . . . . 7 ((2nd :V⟶V ∧ 𝑥𝑋 ({𝑥} × 𝐶) ⊆ V) → (2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)⟶V)
4542, 43, 44mp2an 690 . . . . . 6 (2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)⟶V
46 ffn 6717 . . . . . 6 ((2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)⟶V → (2nd 𝑥𝑋 ({𝑥} × 𝐶)) Fn 𝑥𝑋 ({𝑥} × 𝐶))
4745, 46mp1i 13 . . . . 5 (𝜑 → (2nd 𝑥𝑋 ({𝑥} × 𝐶)) Fn 𝑥𝑋 ({𝑥} × 𝐶))
48 djussxp2 32479 . . . . . . . 8 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝑥𝑋 𝐶)
49 imass2 6101 . . . . . . . 8 ( 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝑥𝑋 𝐶) → (2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ (2nd “ (𝑋 × 𝑥𝑋 𝐶)))
5048, 49ax-mp 5 . . . . . . 7 (2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ (2nd “ (𝑋 × 𝑥𝑋 𝐶))
51 ima0 6075 . . . . . . . . . . 11 (2nd “ ∅) = ∅
52 xpeq1 5686 . . . . . . . . . . . . 13 (𝑋 = ∅ → (𝑋 × 𝑥𝑋 𝐶) = (∅ × 𝑥𝑋 𝐶))
53 0xp 5770 . . . . . . . . . . . . 13 (∅ × 𝑥𝑋 𝐶) = ∅
5452, 53eqtrdi 2781 . . . . . . . . . . . 12 (𝑋 = ∅ → (𝑋 × 𝑥𝑋 𝐶) = ∅)
5554imaeq2d 6058 . . . . . . . . . . 11 (𝑋 = ∅ → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = (2nd “ ∅))
56 iuneq1 5007 . . . . . . . . . . . 12 (𝑋 = ∅ → 𝑥𝑋 𝐶 = 𝑥 ∈ ∅ 𝐶)
57 0iun 5061 . . . . . . . . . . . 12 𝑥 ∈ ∅ 𝐶 = ∅
5856, 57eqtrdi 2781 . . . . . . . . . . 11 (𝑋 = ∅ → 𝑥𝑋 𝐶 = ∅)
5951, 55, 583eqtr4a 2791 . . . . . . . . . 10 (𝑋 = ∅ → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = 𝑥𝑋 𝐶)
6059adantl 480 . . . . . . . . 9 ((𝜑𝑋 = ∅) → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = 𝑥𝑋 𝐶)
61 2ndimaxp 32478 . . . . . . . . . 10 (𝑋 ≠ ∅ → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = 𝑥𝑋 𝐶)
6261adantl 480 . . . . . . . . 9 ((𝜑𝑋 ≠ ∅) → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = 𝑥𝑋 𝐶)
6360, 62pm2.61dane 3019 . . . . . . . 8 (𝜑 → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = 𝑥𝑋 𝐶)
6463, 10eqtrd 2765 . . . . . . 7 (𝜑 → (2nd “ (𝑋 × 𝑥𝑋 𝐶)) = 𝐴)
6550, 64sseqtrid 4025 . . . . . 6 (𝜑 → (2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ 𝐴)
66 resssxp 6269 . . . . . 6 ((2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ 𝐴 ↔ (2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ ( 𝑥𝑋 ({𝑥} × 𝐶) × 𝐴))
6765, 66sylib 217 . . . . 5 (𝜑 → (2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ ( 𝑥𝑋 ({𝑥} × 𝐶) × 𝐴))
68 dff2 7104 . . . . 5 ((2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)⟶𝐴 ↔ ((2nd 𝑥𝑋 ({𝑥} × 𝐶)) Fn 𝑥𝑋 ({𝑥} × 𝐶) ∧ (2nd 𝑥𝑋 ({𝑥} × 𝐶)) ⊆ ( 𝑥𝑋 ({𝑥} × 𝐶) × 𝐴)))
6947, 67, 68sylanbrc 581 . . . 4 (𝜑 → (2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)⟶𝐴)
705, 69fcod 6744 . . 3 (𝜑 → (𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶))): 𝑥𝑋 ({𝑥} × 𝐶)⟶𝐵)
717, 4, 8, 9, 102ndresdju 32480 . . . 4 (𝜑 → (2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)–1-1𝐴)
722fvexi 6906 . . . . 5 0 ∈ V
7372a1i 11 . . . 4 (𝜑0 ∈ V)
745, 4fexd 7235 . . . 4 (𝜑𝐹 ∈ V)
756, 71, 73, 74fsuppco 9425 . . 3 (𝜑 → (𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶))) finSupp 0 )
761, 2, 3, 25, 30, 8, 39, 70, 75gsum2d 19931 . 2 (𝜑 → (𝐺 Σg (𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))) = (𝐺 Σg (𝑦𝑋 ↦ (𝐺 Σg (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧))))))
77 nfcsb1v 3909 . . . . . . . . 9 𝑥𝑦 / 𝑥𝐶
78 csbeq1a 3898 . . . . . . . . 9 (𝑥 = 𝑦𝐶 = 𝑦 / 𝑥𝐶)
798, 21, 77, 78iunsnima2 32454 . . . . . . . 8 ((𝜑𝑦𝑋) → ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) = 𝑦 / 𝑥𝐶)
80 df-ov 7419 . . . . . . . . 9 (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧) = ((𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))‘⟨𝑦, 𝑧⟩)
8169ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (2nd 𝑥𝑋 ({𝑥} × 𝐶)): 𝑥𝑋 ({𝑥} × 𝐶)⟶𝐴)
82 simplr 767 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑦𝑋)
83 vsnid 4661 . . . . . . . . . . . . . . 15 𝑦 ∈ {𝑦}
8483a1i 11 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑦 ∈ {𝑦})
8579eleq2d 2811 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝑋) → (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↔ 𝑧𝑦 / 𝑥𝐶))
8685biimpa 475 . . . . . . . . . . . . . 14 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑧𝑦 / 𝑥𝐶)
8784, 86opelxpd 5711 . . . . . . . . . . . . 13 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ⟨𝑦, 𝑧⟩ ∈ ({𝑦} × 𝑦 / 𝑥𝐶))
88 nfcv 2892 . . . . . . . . . . . . . . . 16 𝑥{𝑦}
8988, 77nfxp 5705 . . . . . . . . . . . . . . 15 𝑥({𝑦} × 𝑦 / 𝑥𝐶)
9089nfel2 2911 . . . . . . . . . . . . . 14 𝑥𝑦, 𝑧⟩ ∈ ({𝑦} × 𝑦 / 𝑥𝐶)
91 sneq 4634 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → {𝑥} = {𝑦})
9291, 78xpeq12d 5703 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → ({𝑥} × 𝐶) = ({𝑦} × 𝑦 / 𝑥𝐶))
9392eleq2d 2811 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (⟨𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶) ↔ ⟨𝑦, 𝑧⟩ ∈ ({𝑦} × 𝑦 / 𝑥𝐶)))
9490, 93rspce 3590 . . . . . . . . . . . . 13 ((𝑦𝑋 ∧ ⟨𝑦, 𝑧⟩ ∈ ({𝑦} × 𝑦 / 𝑥𝐶)) → ∃𝑥𝑋𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶))
9582, 87, 94syl2anc 582 . . . . . . . . . . . 12 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ∃𝑥𝑋𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶))
96 eliun 4995 . . . . . . . . . . . 12 (⟨𝑦, 𝑧⟩ ∈ 𝑥𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥𝑋𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶))
9795, 96sylibr 233 . . . . . . . . . . 11 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ⟨𝑦, 𝑧⟩ ∈ 𝑥𝑋 ({𝑥} × 𝐶))
9881, 97fvco3d 6993 . . . . . . . . . 10 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))‘⟨𝑦, 𝑧⟩) = (𝐹‘((2nd 𝑥𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩)))
9997fvresd 6912 . . . . . . . . . . . 12 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((2nd 𝑥𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩) = (2nd ‘⟨𝑦, 𝑧⟩))
100 vex 3467 . . . . . . . . . . . . 13 𝑦 ∈ V
101 vex 3467 . . . . . . . . . . . . 13 𝑧 ∈ V
102100, 101op2nd 8000 . . . . . . . . . . . 12 (2nd ‘⟨𝑦, 𝑧⟩) = 𝑧
10399, 102eqtrdi 2781 . . . . . . . . . . 11 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((2nd 𝑥𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩) = 𝑧)
104103fveq2d 6896 . . . . . . . . . 10 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (𝐹‘((2nd 𝑥𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩)) = (𝐹𝑧))
10598, 104eqtrd 2765 . . . . . . . . 9 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))‘⟨𝑦, 𝑧⟩) = (𝐹𝑧))
10680, 105eqtrid 2777 . . . . . . . 8 (((𝜑𝑦𝑋) ∧ 𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧) = (𝐹𝑧))
10779, 106mpteq12dva 5232 . . . . . . 7 ((𝜑𝑦𝑋) → (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧)) = (𝑧𝑦 / 𝑥𝐶 ↦ (𝐹𝑧)))
1085adantr 479 . . . . . . . 8 ((𝜑𝑦𝑋) → 𝐹:𝐴𝐵)
109 imassrn 6069 . . . . . . . . . 10 ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ⊆ ran 𝑥𝑋 ({𝑥} × 𝐶)
11010xpeq2d 5702 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 × 𝑥𝑋 𝐶) = (𝑋 × 𝐴))
11148, 110sseqtrid 4025 . . . . . . . . . . . . 13 (𝜑 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴))
112 rnss 5935 . . . . . . . . . . . . 13 ( 𝑥𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴) → ran 𝑥𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴))
113111, 112syl 17 . . . . . . . . . . . 12 (𝜑 → ran 𝑥𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴))
114113adantr 479 . . . . . . . . . . 11 ((𝜑𝑦𝑋) → ran 𝑥𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴))
115 rnxpss 6171 . . . . . . . . . . 11 ran (𝑋 × 𝐴) ⊆ 𝐴
116114, 115sstrdi 3985 . . . . . . . . . 10 ((𝜑𝑦𝑋) → ran 𝑥𝑋 ({𝑥} × 𝐶) ⊆ 𝐴)
117109, 116sstrid 3984 . . . . . . . . 9 ((𝜑𝑦𝑋) → ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ⊆ 𝐴)
11879, 117eqsstrrd 4012 . . . . . . . 8 ((𝜑𝑦𝑋) → 𝑦 / 𝑥𝐶𝐴)
119108, 118feqresmpt 6963 . . . . . . 7 ((𝜑𝑦𝑋) → (𝐹𝑦 / 𝑥𝐶) = (𝑧𝑦 / 𝑥𝐶 ↦ (𝐹𝑧)))
120107, 119eqtr4d 2768 . . . . . 6 ((𝜑𝑦𝑋) → (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧)) = (𝐹𝑦 / 𝑥𝐶))
121120oveq2d 7432 . . . . 5 ((𝜑𝑦𝑋) → (𝐺 Σg (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧))) = (𝐺 Σg (𝐹𝑦 / 𝑥𝐶)))
122121mpteq2dva 5243 . . . 4 (𝜑 → (𝑦𝑋 ↦ (𝐺 Σg (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧)))) = (𝑦𝑋 ↦ (𝐺 Σg (𝐹𝑦 / 𝑥𝐶))))
123 nfcv 2892 . . . . 5 𝑦(𝐺 Σg (𝐹𝐶))
124 nfcv 2892 . . . . . 6 𝑥𝐺
125 nfcv 2892 . . . . . 6 𝑥 Σg
126 nfcv 2892 . . . . . . 7 𝑥𝐹
127126, 77nfres 5981 . . . . . 6 𝑥(𝐹𝑦 / 𝑥𝐶)
128124, 125, 127nfov 7446 . . . . 5 𝑥(𝐺 Σg (𝐹𝑦 / 𝑥𝐶))
12978reseq2d 5979 . . . . . 6 (𝑥 = 𝑦 → (𝐹𝐶) = (𝐹𝑦 / 𝑥𝐶))
130129oveq2d 7432 . . . . 5 (𝑥 = 𝑦 → (𝐺 Σg (𝐹𝐶)) = (𝐺 Σg (𝐹𝑦 / 𝑥𝐶)))
131123, 128, 130cbvmpt 5254 . . . 4 (𝑥𝑋 ↦ (𝐺 Σg (𝐹𝐶))) = (𝑦𝑋 ↦ (𝐺 Σg (𝐹𝑦 / 𝑥𝐶)))
132122, 131eqtr4di 2783 . . 3 (𝜑 → (𝑦𝑋 ↦ (𝐺 Σg (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧)))) = (𝑥𝑋 ↦ (𝐺 Σg (𝐹𝐶))))
133132oveq2d 7432 . 2 (𝜑 → (𝐺 Σg (𝑦𝑋 ↦ (𝐺 Σg (𝑧 ∈ ( 𝑥𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd 𝑥𝑋 ({𝑥} × 𝐶)))𝑧))))) = (𝐺 Σg (𝑥𝑋 ↦ (𝐺 Σg (𝐹𝐶)))))
13412, 76, 1333eqtrd 2769 1 (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥𝑋 ↦ (𝐺 Σg (𝐹𝐶)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wcel 2098  wne 2930  wral 3051  wrex 3060  Vcvv 3463  csb 3884  wss 3939  c0 4318  {csn 4624  cop 4630   ciun 4991  Disj wdisj 5108   class class class wbr 5143  cmpt 5226   × cxp 5670  dom cdm 5672  ran crn 5673  cres 5674  cima 5675  ccom 5676  Rel wrel 5677   Fn wfn 6538  wf 6539  ontowfo 6541  cfv 6543  (class class class)co 7416  2nd c2nd 7990   finSupp cfsupp 9385  Basecbs 17179  0gc0g 17420   Σg cgsu 17421  CMndccmn 19739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-disj 5109  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-om 7869  df-1st 7991  df-2nd 7992  df-supp 8164  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-fsupp 9386  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-n0 12503  df-z 12589  df-uz 12853  df-fz 13517  df-fzo 13660  df-seq 13999  df-hash 14322  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-0g 17422  df-gsum 17423  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18740  df-mulg 19028  df-cntz 19272  df-cmn 19741
This theorem is referenced by:  elrspunidl  33193
  Copyright terms: Public domain W3C validator