tsmsf1o

Description: Re-index an infinite group sum using a bijection. (Contributed by Mario Carneiro, 18-Sep-2015)

	Ref	Expression
Hypotheses	tsmsf1o.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tsmsf1o.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	tsmsf1o.2	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
	tsmsf1o.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	tsmsf1o.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	tsmsf1o.s	⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
Assertion	tsmsf1o	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( 𝐺 tsums ( 𝐹 ∘ 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tsmsf1o.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tsmsf1o.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3		tsmsf1o.2	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
4		tsmsf1o.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		tsmsf1o.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6		tsmsf1o.s	⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
7		f1opwfi	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) )
8	6 7	syl	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) )
9		f1of	⊢ ( ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) → ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) ⟶ ( 𝒫 𝐴 ∩ Fin ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) ⟶ ( 𝒫 𝐴 ∩ Fin ) )
11		eqid	⊢ ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) = ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) )
12	11	fmpt	⊢ ( ∀ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐻 “ 𝑎 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) ⟶ ( 𝒫 𝐴 ∩ Fin ) )
13	10 12	sylibr	⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐻 “ 𝑎 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
14		sseq1	⊢ ( 𝑦 = ( 𝐻 “ 𝑎 ) → ( 𝑦 ⊆ 𝑧 ↔ ( 𝐻 “ 𝑎 ) ⊆ 𝑧 ) )
15	14	imbi1d	⊢ ( 𝑦 = ( 𝐻 “ 𝑎 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
16	15	ralbidv	⊢ ( 𝑦 = ( 𝐻 “ 𝑎 ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
17	11 16	rexrnmptw	⊢ ( ∀ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐻 “ 𝑎 ) ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ∃ 𝑦 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
18	13 17	syl	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
19		f1ofo	⊢ ( ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) –1-1-onto→ ( 𝒫 𝐴 ∩ Fin ) → ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) –onto→ ( 𝒫 𝐴 ∩ Fin ) )
20		forn	⊢ ( ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) –onto→ ( 𝒫 𝐴 ∩ Fin ) → ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) = ( 𝒫 𝐴 ∩ Fin ) )
21	8 19 20	3syl	⊢ ( 𝜑 → ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) = ( 𝒫 𝐴 ∩ Fin ) )
22	21	rexeqdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
23		imaeq2	⊢ ( 𝑎 = 𝑏 → ( 𝐻 “ 𝑎 ) = ( 𝐻 “ 𝑏 ) )
24	23	cbvmptv	⊢ ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) = ( 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑏 ) )
25	24	fmpt	⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐻 “ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) : ( 𝒫 𝐶 ∩ Fin ) ⟶ ( 𝒫 𝐴 ∩ Fin ) )
26	10 25	sylibr	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐻 “ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) )
27		sseq2	⊢ ( 𝑧 = ( 𝐻 “ 𝑏 ) → ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 ↔ ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) ) )
28		reseq2	⊢ ( 𝑧 = ( 𝐻 “ 𝑏 ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) )
29	28	oveq2d	⊢ ( 𝑧 = ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) )
30	29	eleq1d	⊢ ( 𝑧 = ( 𝐻 “ 𝑏 ) → ( ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) )
31	27 30	imbi12d	⊢ ( 𝑧 = ( 𝐻 “ 𝑏 ) → ( ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ) )
32	24 31	ralrnmptw	⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝐻 “ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ∀ 𝑧 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ) )
33	26 32	syl	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ) )
34	21	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↦ ( 𝐻 “ 𝑎 ) ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
35	33 34	bitr3d	⊢ ( 𝜑 → ( ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ↔ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ↔ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) )
37		f1of1	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 –1-1→ 𝐴 )
38	6 37	syl	⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1→ 𝐴 )
39	38	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐻 : 𝐶 –1-1→ 𝐴 )
40		elfpw	⊢ ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝑎 ⊆ 𝐶 ∧ 𝑎 ∈ Fin ) )
41	40	simplbi	⊢ ( 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑎 ⊆ 𝐶 )
42	41	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑎 ⊆ 𝐶 )
43		elfpw	⊢ ( 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ↔ ( 𝑏 ⊆ 𝐶 ∧ 𝑏 ∈ Fin ) )
44	43	simplbi	⊢ ( 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑏 ⊆ 𝐶 )
45	44	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑏 ⊆ 𝐶 )
46		f1imass	⊢ ( ( 𝐻 : 𝐶 –1-1→ 𝐴 ∧ ( 𝑎 ⊆ 𝐶 ∧ 𝑏 ⊆ 𝐶 ) ) → ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) ↔ 𝑎 ⊆ 𝑏 ) )
47	39 42 45 46	syl12anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) ↔ 𝑎 ⊆ 𝑏 ) )
48		eqid	⊢ ( 0_g ‘ 𝐺 ) = ( 0_g ‘ 𝐺 )
49	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐺 ∈ CMnd )
50		elinel2	⊢ ( 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) → 𝑏 ∈ Fin )
51	50	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝑏 ∈ Fin )
52		f1ores	⊢ ( ( 𝐻 : 𝐶 –1-1→ 𝐴 ∧ 𝑏 ⊆ 𝐶 ) → ( 𝐻 ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐻 “ 𝑏 ) )
53	39 45 52	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐻 ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐻 “ 𝑏 ) )
54		f1ofo	⊢ ( ( 𝐻 ↾ 𝑏 ) : 𝑏 –1-1-onto→ ( 𝐻 “ 𝑏 ) → ( 𝐻 ↾ 𝑏 ) : 𝑏 –onto→ ( 𝐻 “ 𝑏 ) )
55	53 54	syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐻 ↾ 𝑏 ) : 𝑏 –onto→ ( 𝐻 “ 𝑏 ) )
56		fofi	⊢ ( ( 𝑏 ∈ Fin ∧ ( 𝐻 ↾ 𝑏 ) : 𝑏 –onto→ ( 𝐻 “ 𝑏 ) ) → ( 𝐻 “ 𝑏 ) ∈ Fin )
57	51 55 56	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐻 “ 𝑏 ) ∈ Fin )
58	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
59		imassrn	⊢ ( 𝐻 “ 𝑏 ) ⊆ ran 𝐻
60	6	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → 𝐻 : 𝐶 –1-1-onto→ 𝐴 )
61		f1ofo	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 –onto→ 𝐴 )
62		forn	⊢ ( 𝐻 : 𝐶 –onto→ 𝐴 → ran 𝐻 = 𝐴 )
63	60 61 62	3syl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ran 𝐻 = 𝐴 )
64	59 63	sseqtrid	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐻 “ 𝑏 ) ⊆ 𝐴 )
65	58 64	fssresd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) : ( 𝐻 “ 𝑏 ) ⟶ 𝐵 )
66		fvexd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 0_g ‘ 𝐺 ) ∈ V )
67	65 57 66	fdmfifsupp	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) finSupp ( 0_g ‘ 𝐺 ) )
68	1 48 49 57 65 67 53	gsumf1o	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) = ( 𝐺 Σ_g ( ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ∘ ( 𝐻 ↾ 𝑏 ) ) ) )
69		df-ima	⊢ ( 𝐻 “ 𝑏 ) = ran ( 𝐻 ↾ 𝑏 )
70	69	eqimss2i	⊢ ran ( 𝐻 ↾ 𝑏 ) ⊆ ( 𝐻 “ 𝑏 )
71		cores	⊢ ( ran ( 𝐻 ↾ 𝑏 ) ⊆ ( 𝐻 “ 𝑏 ) → ( ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ∘ ( 𝐻 ↾ 𝑏 ) ) = ( 𝐹 ∘ ( 𝐻 ↾ 𝑏 ) ) )
72	70 71	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ∘ ( 𝐻 ↾ 𝑏 ) ) = ( 𝐹 ∘ ( 𝐻 ↾ 𝑏 ) )
73		resco	⊢ ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) = ( 𝐹 ∘ ( 𝐻 ↾ 𝑏 ) )
74	72 73	eqtr4i	⊢ ( ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ∘ ( 𝐻 ↾ 𝑏 ) ) = ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 )
75	74	oveq2i	⊢ ( 𝐺 Σ_g ( ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ∘ ( 𝐻 ↾ 𝑏 ) ) ) = ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) )
76	68 75	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) = ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) )
77	76	eleq1d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ↔ ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) )
78	47 77	imbi12d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ↔ ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
79	78	ralbidva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ ( 𝐻 “ 𝑏 ) → ( 𝐺 Σ_g ( 𝐹 ↾ ( 𝐻 “ 𝑏 ) ) ) ∈ 𝑢 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
80	36 79	bitr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
81	80	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( ( 𝐻 “ 𝑎 ) ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
82	18 22 81	3bitr3d	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) )
83	82	imbi2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
84	83	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) )
85	84	anbi2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) )
86		eqid	⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 )
87		eqid	⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
88	1 86 87 2 3 4 5	eltsms	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σ_g ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) )
89		eqid	⊢ ( 𝒫 𝐶 ∩ Fin ) = ( 𝒫 𝐶 ∩ Fin )
90		f1dmex	⊢ ( ( 𝐻 : 𝐶 –1-1→ 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐶 ∈ V )
91	38 4 90	syl2anc	⊢ ( 𝜑 → 𝐶 ∈ V )
92		f1of	⊢ ( 𝐻 : 𝐶 –1-1-onto→ 𝐴 → 𝐻 : 𝐶 ⟶ 𝐴 )
93	6 92	syl	⊢ ( 𝜑 → 𝐻 : 𝐶 ⟶ 𝐴 )
94		fco	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐻 : 𝐶 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 )
95	5 93 94	syl2anc	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) : 𝐶 ⟶ 𝐵 )
96	1 86 89 2 3 91 95	eltsms	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ∘ 𝐻 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 𝐶 ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 𝐶 ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σ_g ( ( 𝐹 ∘ 𝐻 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) )
97	85 88 96	3bitr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ∘ 𝐻 ) ) ) )
98	97	eqrdv	⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( 𝐺 tsums ( 𝐹 ∘ 𝐻 ) ) )

Metamath Proof Explorer

Theorem tsmsf1o

Proof