Metamath Proof Explorer

Theorem tsmsval2

Description: Definition of the topological group sum(s) of a collection F ( x ) of values in the group with index set A . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tsmsval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmsval.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tsmsval.s ⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
tsmsval.l ⊢ 𝐿 = ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
tsmsval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
tsmsval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
tsmsval2.a ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
Assertion tsmsval2 ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tsmsval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 tsmsval.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 tsmsval.s ⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
4 tsmsval.l ⊢ 𝐿 = ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
5 tsmsval.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
6 tsmsval2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑊 )
7 tsmsval2.a ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
8 df-tsms ⊢ tsums = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) )
9 8 a1i ⊢ ( 𝜑 → tsums = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) ) )
10 vex ⊢ 𝑓 ∈ V
11 10 dmex ⊢ dom 𝑓 ∈ V
12 11 pwex ⊢ 𝒫 dom 𝑓 ∈ V
13 12 inex1 ⊢ ( 𝒫 dom 𝑓 ∩ Fin ) ∈ V
14 13 a1i ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝒫 dom 𝑓 ∩ Fin ) ∈ V )
15 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → 𝑤 = 𝐺 )
16 15 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( TopOpen ‘ 𝑤 ) = ( TopOpen ‘ 𝐺 ) )
17 16 2 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( TopOpen ‘ 𝑤 ) = 𝐽 )
18 id ⊢ ( 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) → 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) )
19 simprr ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝑓 = 𝐹 )
20 19 dmeqd ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom 𝑓 = dom 𝐹 )
21 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom 𝐹 = 𝐴 )
22 20 21 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → dom 𝑓 = 𝐴 )
23 22 pweqd ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → 𝒫 dom 𝑓 = 𝒫 𝐴 )
24 23 ineq1d ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝒫 dom 𝑓 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin ) )
25 24 3 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ( 𝒫 dom 𝑓 ∩ Fin ) = 𝑆 )
26 18 25 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → 𝑠 = 𝑆 )
27 26 rabeqdv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
28 26 27 mpteq12dv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
29 28 rneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) = ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
30 29 4 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) = 𝐿 )
31 26 30 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) = ( 𝑆 filGen 𝐿 ) )
32 17 31 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) = ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) )
33 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → 𝑓 = 𝐹 )
34 33 reseq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( 𝑓 ↾ 𝑦 ) = ( 𝐹 ↾ 𝑦 ) )
35 15 34 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) )
36 26 35 mpteq12dv ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) )
37 32 36 fveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑠 = ( 𝒫 dom 𝑓 ∩ Fin ) ) → ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) = ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
38 14 37 csbied ⊢ ( ( 𝜑 ∧ ( 𝑤 = 𝐺 ∧ 𝑓 = 𝐹 ) ) → ⦋ ( 𝒫 dom 𝑓 ∩ Fin ) / 𝑠 ⦌ ( ( ( TopOpen ‘ 𝑤 ) fLimf ( 𝑠 filGen ran ( 𝑧 ∈ 𝑠 ↦ { 𝑦 ∈ 𝑠 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑠 ↦ ( 𝑤 Σg ( 𝑓 ↾ 𝑦 ) ) ) ) = ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
39 5 elexd ⊢ ( 𝜑 → 𝐺 ∈ V )
40 6 elexd ⊢ ( 𝜑 → 𝐹 ∈ V )
41 fvexd ⊢ ( 𝜑 → ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ∈ V )
42 9 38 39 40 41 ovmpod ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( 𝑆 filGen 𝐿 ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )