Metamath Proof Explorer

Theorem gsumpart

Description: Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses 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 gsumpart ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumpart.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumpart.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsumpart.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsumpart.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 gsumpart.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
6 gsumpart.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 gsumpart.w ⊢ ( 𝜑 → 𝐹 finSupp 0 )
8 gsumpart.1 ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝐶 )
9 gsumpart.2 ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 )
10 eqid ⊢ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) = ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
11 10 4 5 8 9 2ndresdjuf1o ⊢ ( 𝜑 → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) –1-1-onto→ 𝐴 )
12 1 2 3 4 6 7 11 gsumf1o ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) ) )
13 snex ⊢ { 𝑥 } ∈ V
14 13 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ V )
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 )
16 ssidd ⊢ ( 𝜑 → 𝐴 ⊆ 𝐴 )
17 9 16 eqsstrd ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴 )
18 iunss ⊢ ( ∪ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴 ↔ ∀ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴 )
19 17 18 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴 )
20 19 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ⊆ 𝐴 )
21 15 20 ssexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ V )
22 14 21 xpexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( { 𝑥 } × 𝐶 ) ∈ V )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ∈ V )
24 iunexg ⊢ ( ( 𝑋 ∈ 𝑊 ∧ ∀ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ∈ V ) → ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ∈ V )
25 5 23 24 syl2anc ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ∈ V )
26 relxp ⊢ Rel ( { 𝑥 } × 𝐶 )
27 26 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Rel ( { 𝑥 } × 𝐶 ) )
28 27 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 Rel ( { 𝑥 } × 𝐶 ) )
29 reliun ⊢ ( Rel ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ↔ ∀ 𝑥 ∈ 𝑋 Rel ( { 𝑥 } × 𝐶 ) )
30 28 29 sylibr ⊢ ( 𝜑 → Rel ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) )
31 dmiun ⊢ dom ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) = ∪ 𝑥 ∈ 𝑋 dom ( { 𝑥 } × 𝐶 )
32 dmxpss ⊢ dom ( { 𝑥 } × 𝐶 ) ⊆ { 𝑥 }
33 32 rgenw ⊢ ∀ 𝑥 ∈ 𝑋 dom ( { 𝑥 } × 𝐶 ) ⊆ { 𝑥 }
34 ss2iun ⊢ ( ∀ 𝑥 ∈ 𝑋 dom ( { 𝑥 } × 𝐶 ) ⊆ { 𝑥 } → ∪ 𝑥 ∈ 𝑋 dom ( { 𝑥 } × 𝐶 ) ⊆ ∪ 𝑥 ∈ 𝑋 { 𝑥 } )
35 33 34 ax-mp ⊢ ∪ 𝑥 ∈ 𝑋 dom ( { 𝑥 } × 𝐶 ) ⊆ ∪ 𝑥 ∈ 𝑋 { 𝑥 }
36 31 35 eqsstri ⊢ dom ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ∪ 𝑥 ∈ 𝑋 { 𝑥 }
37 iunid ⊢ ∪ 𝑥 ∈ 𝑋 { 𝑥 } = 𝑋
38 36 37 sseqtri ⊢ dom ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ 𝑋
39 38 a1i ⊢ ( 𝜑 → dom ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ 𝑋 )
40 fo2nd ⊢ 2nd : V –onto→ V
41 fof ⊢ ( 2nd : V –onto→ V → 2nd : V ⟶ V )
42 40 41 ax-mp ⊢ 2nd : V ⟶ V
43 ssv ⊢ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ V
44 fssres ⊢ ( ( 2nd : V ⟶ V ∧ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ V ) → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ V )
45 42 43 44 mp2an ⊢ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ V
46 ffn ⊢ ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ V → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) Fn ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) )
47 45 46 mp1i ⊢ ( 𝜑 → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) Fn ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) )
48 djussxp2 ⊢ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 )
49 imass2 ⊢ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) → ( 2nd “ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) )
50 48 49 ax-mp ⊢ ( 2nd “ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) )
51 ima0 ⊢ ( 2nd “ ∅ ) = ∅
52 xpeq1 ⊢ ( 𝑋 = ∅ → ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) = ( ∅ × ∪ 𝑥 ∈ 𝑋 𝐶 ) )
53 0xp ⊢ ( ∅ × ∪ 𝑥 ∈ 𝑋 𝐶 ) = ∅
54 52 53 eqtrdi ⊢ ( 𝑋 = ∅ → ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) = ∅ )
55 54 imaeq2d ⊢ ( 𝑋 = ∅ → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = ( 2nd “ ∅ ) )
56 iuneq1 ⊢ ( 𝑋 = ∅ → ∪ 𝑥 ∈ 𝑋 𝐶 = ∪ 𝑥 ∈ ∅ 𝐶 )
57 0iun ⊢ ∪ 𝑥 ∈ ∅ 𝐶 = ∅
58 56 57 eqtrdi ⊢ ( 𝑋 = ∅ → ∪ 𝑥 ∈ 𝑋 𝐶 = ∅ )
59 51 55 58 3eqtr4a ⊢ ( 𝑋 = ∅ → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = ∪ 𝑥 ∈ 𝑋 𝐶 )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = ∪ 𝑥 ∈ 𝑋 𝐶 )
61 2ndimaxp ⊢ ( 𝑋 ≠ ∅ → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = ∪ 𝑥 ∈ 𝑋 𝐶 )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ≠ ∅ ) → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = ∪ 𝑥 ∈ 𝑋 𝐶 )
63 60 62 pm2.61dane ⊢ ( 𝜑 → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = ∪ 𝑥 ∈ 𝑋 𝐶 )
64 63 9 eqtrd ⊢ ( 𝜑 → ( 2nd “ ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) ) = 𝐴 )
65 50 64 sseqtrid ⊢ ( 𝜑 → ( 2nd “ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ 𝐴 )
66 resssxp ⊢ ( ( 2nd “ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ 𝐴 ↔ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) × 𝐴 ) )
67 65 66 sylib ⊢ ( 𝜑 → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) × 𝐴 ) )
68 dff2 ⊢ ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ 𝐴 ↔ ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) Fn ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ∧ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ⊆ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) × 𝐴 ) ) )
69 47 67 68 sylanbrc ⊢ ( 𝜑 → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ 𝐴 )
70 6 69 fcod ⊢ ( 𝜑 → ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ 𝐵 )
71 10 4 5 8 9 2ndresdju ⊢ ( 𝜑 → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) –1-1→ 𝐴 )
72 2 fvexi ⊢ 0 ∈ V
73 72 a1i ⊢ ( 𝜑 → 0 ∈ V )
74 6 4 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
75 7 71 73 74 fsuppco ⊢ ( 𝜑 → ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) finSupp 0 )
76 1 2 3 25 30 5 39 70 75 gsum2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) ) ) ) )
77 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
78 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
79 5 21 77 78 iunsnima2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
80 df-ov ⊢ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) = ( ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ )
81 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) : ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⟶ 𝐴 )
82 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → 𝑦 ∈ 𝑋 )
83 vsnid ⊢ 𝑦 ∈ { 𝑦 }
84 83 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → 𝑦 ∈ { 𝑦 } )
85 79 eleq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↔ 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
86 85 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
87 84 86 opelxpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
88 nfcv ⊢ Ⅎ 𝑥 { 𝑦 }
89 88 77 nfxp ⊢ Ⅎ 𝑥 ( { 𝑦 } × ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
90 89 nfel2 ⊢ Ⅎ 𝑥 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
91 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
92 91 78 xpeq12d ⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } × 𝐶 ) = ( { 𝑦 } × ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
93 92 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝐶 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
94 90 93 rspce ⊢ ( ( 𝑦 ∈ 𝑋 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑦 } × ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) → ∃ 𝑥 ∈ 𝑋 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝐶 ) )
95 82 87 94 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ∃ 𝑥 ∈ 𝑋 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝐶 ) )
96 eliun ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝑋 ⟨ 𝑦 , 𝑧 ⟩ ∈ ( { 𝑥 } × 𝐶 ) )
97 95 96 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) )
98 81 97 fvco3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = ( 𝐹 ‘ ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) )
99 97 fvresd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
100 vex ⊢ 𝑦 ∈ V
101 vex ⊢ 𝑧 ∈ V
102 100 101 op2nd ⊢ ( 2nd ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = 𝑧
103 99 102 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = 𝑧 )
104 103 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( 𝐹 ‘ ( ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) ) = ( 𝐹 ‘ 𝑧 ) )
105 98 104 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) ‘ ⟨ 𝑦 , 𝑧 ⟩ ) = ( 𝐹 ‘ 𝑧 ) )
106 80 105 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ) → ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
107 79 106 mpteq12dva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) = ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↦ ( 𝐹 ‘ 𝑧 ) ) )
108 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
109 imassrn ⊢ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ⊆ ran ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
110 9 xpeq2d ⊢ ( 𝜑 → ( 𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶 ) = ( 𝑋 × 𝐴 ) )
111 48 110 sseqtrid ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × 𝐴 ) )
112 rnss ⊢ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ( 𝑋 × 𝐴 ) → ran ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ran ( 𝑋 × 𝐴 ) )
113 111 112 syl ⊢ ( 𝜑 → ran ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ran ( 𝑋 × 𝐴 ) )
114 113 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ran ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ ran ( 𝑋 × 𝐴 ) )
115 rnxpss ⊢ ran ( 𝑋 × 𝐴 ) ⊆ 𝐴
116 114 115 sstrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ran ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ⊆ 𝐴 )
117 109 116 sstrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ⊆ 𝐴 )
118 79 117 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ⊆ 𝐴 )
119 108 118 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↦ ( 𝐹 ‘ 𝑧 ) ) )
120 107 119 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) = ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
121 120 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐺 Σg ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) ) = ( 𝐺 Σg ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
122 121 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) )
123 nfcv ⊢ Ⅎ 𝑦 ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) )
124 nfcv ⊢ Ⅎ 𝑥 𝐺
125 nfcv ⊢ Ⅎ 𝑥 Σg
126 nfcv ⊢ Ⅎ 𝑥 𝐹
127 126 77 nfres ⊢ Ⅎ 𝑥 ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
128 124 125 127 nfov ⊢ Ⅎ 𝑥 ( 𝐺 Σg ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
129 78 reseq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ↾ 𝐶 ) = ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
130 129 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
131 123 128 130 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
132 122 131 eqtr4di ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ) )
133 132 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑦 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) “ { 𝑦 } ) ↦ ( 𝑦 ( 𝐹 ∘ ( 2nd ↾ ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 ) ) ) 𝑧 ) ) ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ) ) )
134 12 76 133 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) ) ) )