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 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ 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 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
45 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
46 45 16 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 )
47 6 5 fexd ⊢ ( 𝜑 → 𝐹 ∈ V )
48 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 ∈ V )
49 2 fvexi ⊢ 0 ∈ V
50 ressuppss ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
51 48 49 50 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
52 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 )
53 51 52 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ 𝑊 )
54 49 a1i ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ∈ V )
55 46 19 54 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) finSupp 0 )
56 1 2 44 19 46 53 55 gsumres ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) )
57 resres ⊢ ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) )
58 57 oveq2i ⊢ ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) )
59 56 58 eqtr3di ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) )
60 59 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) )
61 43 60 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) )
62 37 61 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
63 62 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
64 sseq1 ⊢ ( 𝑦 = 𝑎 → ( 𝑦 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑧 ) )
65 64 rspceaimv ⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
66 13 63 65 syl6an ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
67 66 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
68 elfpw ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin ) )
69 68 simplbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 )
70 69 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
71 70 ssrind ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) )
72 elinel2 ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
74 inss1 ⊢ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑦
75 ssfi ⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑦 ) → ( 𝑦 ∩ 𝑊 ) ∈ Fin )
76 73 74 75 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ∈ Fin )
77 elfpw ⊢ ( ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( ( 𝑦 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ∧ ( 𝑦 ∩ 𝑊 ) ∈ Fin ) )
78 71 76 77 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) )
79 69 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑦 ⊆ 𝐴 )
80 elfpw ⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) ∧ 𝑏 ∈ Fin ) )
81 80 simplbi ⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) )
82 81 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) )
83 82 8 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ 𝐴 )
84 79 83 unssd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 )
85 elinel2 ⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑏 ∈ Fin )
86 unfi ⊢ ( ( 𝑦 ∈ Fin ∧ 𝑏 ∈ Fin ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin )
87 73 85 86 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin )
88 elfpw ⊢ ( ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 ∧ ( 𝑦 ∪ 𝑏 ) ∈ Fin ) )
89 84 87 88 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
90 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ 𝑏 )
91 id ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → 𝑧 = ( 𝑦 ∪ 𝑏 ) )
92 90 91 sseqtrrid ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → 𝑦 ⊆ 𝑧 )
93 pm5.5 ⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
94 92 93 syl ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) )
95 reseq2 ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) )
96 95 oveq2d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) )
97 96 eleq1d ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
98 94 97 bitrd ⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
99 98 rspcv ⊢ ( ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
100 89 99 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) )
101 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝐺 ∈ CMnd )
102 87 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin )
103 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
104 84 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 )
105 103 104 fssresd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) : ( 𝑦 ∪ 𝑏 ) ⟶ 𝐵 )
106 47 49 jctir ⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 0 ∈ V ) )
107 106 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ∈ V ∧ 0 ∈ V ) )
108 ressuppss ⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
109 107 108 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) )
110 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 )
111 109 110 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ 𝑊 )
112 49 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 0 ∈ V )
113 105 102 112 fdmfifsupp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) finSupp 0 )
114 1 2 101 102 105 111 113 gsumres ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) )
115 resres ⊢ ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( 𝐹 ↾ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) )
116 indir ⊢ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) = ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) )
117 82 41 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ 𝑊 )
118 117 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝑏 ⊆ 𝑊 )
119 dfss2 ⊢ ( 𝑏 ⊆ 𝑊 ↔ ( 𝑏 ∩ 𝑊 ) = 𝑏 )
120 118 119 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑏 ∩ 𝑊 ) = 𝑏 )
121 120 uneq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) = ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) )
122 simprr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 )
123 ssequn1 ⊢ ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ↔ ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) = 𝑏 )
124 122 123 sylib ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) = 𝑏 )
125 121 124 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) = 𝑏 )
126 116 125 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) = 𝑏 )
127 126 reseq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑏 ) )
128 115 127 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑏 ) )
129 118 resabs1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( 𝐹 ↾ 𝑏 ) )
130 128 129 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) )
131 130 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) )
132 114 131 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) )
133 132 eleq1d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
134 133 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
135 134 expr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
136 135 com23 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
137 100 136 syld ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
138 137 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
139 sseq1 ⊢ ( 𝑎 = ( 𝑦 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) )
140 139 rspceaimv ⊢ ( ( ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
141 78 138 140 syl6an ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
142 141 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
143 67 142 impbid ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
144 143 imbi2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) )
145 144 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) )
146 145 anbi2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) )
147 eqid ⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
148 eqid ⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) = ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin )
149 inex1g ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝑊 ) ∈ V )
150 5 149 syl ⊢ ( 𝜑 → ( 𝐴 ∩ 𝑊 ) ∈ V )
151 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
152 6 8 151 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
153 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) )
154 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
155 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
156 6 154 155 3syl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
157 156 reseq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑊 ) )
158 153 157 eqtr3id ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑊 ) )
159 158 feq1d ⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) )
160 152 159 mpbid ⊢ ( 𝜑 → ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 )
161 1 147 148 3 4 150 160 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) )
162 eqid ⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
163 1 147 162 3 4 5 6 eltsms ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) )
164 146 161 163 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) ↔ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) )
165 164 eqrdv ⊢ ( 𝜑 → ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 tsums 𝐹 ) )