Metamath Proof Explorer

Theorem tsmsres

Description: Extend an infinite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 18-Sep-2015) (Revised by AV, 25-Jul-2019)

Ref Expression
Hypotheses tsmsres.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsres.z ⊢ 0 = ( 0g ‘ 𝐺 )
tsmsres.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmsres.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
tsmsres.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmsres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmsres.s ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
Assertion tsmsres ( 𝜑 → ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 tsums 𝐹 ) )

Proof

Step Hyp Ref Expression
1 tsmsres.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmsres.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 tsmsres.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 tsmsres.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
5 tsmsres.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 tsmsres.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 tsmsres.s ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 )
8 inss1 ⊢ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴
9 8 sspwi ⊢ 𝒫 ( 𝐴 ∩ 𝑊 ) ⊆ 𝒫 𝐴
10 ssrin ⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ⊆ 𝒫 𝐴 → ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ Fin ) )
11 9 10 ax-mp ⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ Fin )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) )
13 11 12 sseldi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
14 elfpw ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin ) )
15 14 simplbi ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 )
16 15 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ⊆ 𝐴 )
17 16 ssrind ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑧 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) )
18 elinel2 ⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin )
19 18 adantl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin )
20 inss1 ⊢ ( 𝑧 ∩ 𝑊 ) ⊆ 𝑧
21 ssfi ⊢ ( ( 𝑧 ∈ Fin ∧ ( 𝑧 ∩ 𝑊 ) ⊆ 𝑧 ) → ( 𝑧 ∩ 𝑊 ) ∈ Fin )
22 19 20 21 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑧 ∩ 𝑊 ) ∈ Fin )
23 elfpw ⊢ ( ( 𝑧 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( ( 𝑧 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ∧ ( 𝑧 ∩ 𝑊 ) ∈ Fin ) )
24 17 22 23 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑧 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) )
25 sseq2 ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ( 𝑧 ∩ 𝑊 ) ) )
26 ssin ⊢ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) ↔ 𝑎 ⊆ ( 𝑧 ∩ 𝑊 ) )
27 25 26 bitr4di ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) ) )
28 reseq2 ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( ( 𝐹 ↾ 𝑊 ) ↾ ( 𝑧 ∩ 𝑊 ) ) )
29 inss2 ⊢ ( 𝑧 ∩ 𝑊 ) ⊆ 𝑊
30 resabs1 ⊢ ( ( 𝑧 ∩ 𝑊 ) ⊆ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) ↾ ( 𝑧 ∩ 𝑊 ) ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) )
31 29 30 ax-mp ⊢ ( ( 𝐹 ↾ 𝑊 ) ↾ ( 𝑧 ∩ 𝑊 ) ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) )
32 28 31 eqtrdi ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) )
33 32 oveq2d ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) )
34 33 eleq1d ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) )
35 27 34 imbi12d ⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ↔ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) )
36 35 rspcv ⊢ ( ( 𝑧 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) )
37 24 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) )
38 elfpw ⊢ ( 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( 𝑎 ⊆ ( 𝐴 ∩ 𝑊 ) ∧ 𝑎 ∈ Fin ) )
39 38 simplbi ⊢ ( 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑎 ⊆ ( 𝐴 ∩ 𝑊 ) )
40 39 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ⊆ ( 𝐴 ∩ 𝑊 ) )
41 inss2 ⊢ ( 𝐴 ∩ 𝑊 ) ⊆ 𝑊
42 40 41 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ⊆ 𝑊 )
43 42 biantrud ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑎 ⊆ 𝑧 ↔ ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) ) )
44 resres ⊢ ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) )
45 44 oveq2i ⊢ ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) )
46 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
47 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
48 47 16 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 )
49 fex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V )
50 6 5 49 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ V )
51 50 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 ∈ V )
52 2 fvexi ⊢ 0 ∈ V
53 ressuppss ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
54 51 52 53 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
55 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 )
56 54 55 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ 𝑊 )
57 52 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ∈ V )
58 48 19 57 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) finSupp 0 )
59 1 2 46 19 48 56 58 gsumres ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) )
60 45 59 syl5reqr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) )
61 60 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) )
62 43 61 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) )
63 37 62 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
64 63 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
65 sseq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑧 ) )
66 65 rspceaimv ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
67 13 64 66 syl6an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
68 67 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
69 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin ) )
70 69 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
71 70 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
72 71 ssrind ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) )
73 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
74 73 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
75 inss1 ⊢ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑦
76 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑦 ) → ( 𝑦 ∩ 𝑊 ) ∈ Fin )
77 74 75 76 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ∈ Fin )
78 elfpw ⊢ ( ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( ( 𝑦 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ∧ ( 𝑦 ∩ 𝑊 ) ∈ Fin ) )
79 72 77 78 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) )
80 70 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
81 elfpw ⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) ∧ 𝑏 ∈ Fin ) )
82 81 simplbi ⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) )
83 82 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) )
84 83 8 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ 𝐴 )
85 80 84 unssd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 )
86 elinel2 ⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑏 ∈ Fin )
87 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑏 ∈ Fin ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin )
88 74 86 87 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin )
89 elfpw ⊢ ( ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 ∧ ( 𝑦 ∪ 𝑏 ) ∈ Fin ) )
90 85 88 89 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
91 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ 𝑏 )
92 id ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → 𝑧 = ( 𝑦 ∪ 𝑏 ) )
93 91 92 sseqtrrid ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → 𝑦 ⊆ 𝑧 )
94 pm5.5 ⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
95 93 94 syl ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
96 reseq2 ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) )
97 96 oveq2d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) )
98 97 eleq1d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
99 95 98 bitrd ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
100 99 rspcv ⊢ ( ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
101 90 100 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
102 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝐺 ∈ CMnd )
103 88 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin )
104 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
105 85 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 )
106 104 105 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) : ( 𝑦 ∪ 𝑏 ) ⟶ 𝐵 )
107 50 52 jctir ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 0 ∈ V ) )
108 107 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ∈ V ∧ 0 ∈ V ) )
109 ressuppss ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
110 108 109 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
111 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 )
112 110 111 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ 𝑊 )
113 52 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 0 ∈ V )
114 106 103 113 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) finSupp 0 )
115 1 2 102 103 106 112 114 gsumres ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) )
116 resres ⊢ ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( 𝐹 ↾ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) )
117 indir ⊢ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) = ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) )
118 83 41 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ 𝑊 )
119 118 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝑏 ⊆ 𝑊 )
120 df-ss ⊢ ( 𝑏 ⊆ 𝑊 ↔ ( 𝑏 ∩ 𝑊 ) = 𝑏 )
121 119 120 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑏 ∩ 𝑊 ) = 𝑏 )
122 121 uneq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) = ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) )
123 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 )
124 ssequn1 ⊢ ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ↔ ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) = 𝑏 )
125 123 124 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) = 𝑏 )
126 122 125 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) = 𝑏 )
127 117 126 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) = 𝑏 )
128 127 reseq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑏 ) )
129 116 128 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑏 ) )
130 119 resabs1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( 𝐹 ↾ 𝑏 ) )
131 129 130 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) )
132 131 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) )
133 115 132 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) )
134 133 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
135 134 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
136 135 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
137 136 com23 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
138 101 137 syld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
139 138 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
140 sseq1 ⊢ ( 𝑎 = ( 𝑦 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) )
141 140 rspceaimv ⊢ ( ( ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
142 79 139 141 syl6an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
143 142 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
144 68 143 impbid ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
145 144 imbi2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) )
146 145 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) )
147 146 anbi2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) )
148 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
149 eqid ⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) = ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin )
150 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝑊 ) ∈ V )
151 5 150 syl ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑊 ) ∈ V )
152 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
153 6 8 152 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
154 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) )
155 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
156 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
157 6 155 156 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
158 157 reseq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑊 ) )
159 154 158 syl5eqr ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑊 ) )
160 159 feq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) )
161 153 160 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
162 1 148 149 3 4 151 161 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) )
163 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
164 1 148 163 3 4 5 6 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) )
165 147 162 164 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) ↔ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) )
166 165 eqrdv ⊢ ( 𝜑 → ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 tsums 𝐹 ) )