This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsummptf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018)

Ref Expression
Hypotheses gsummptf1o.x ⊢ Ⅎ 𝑥 𝐻
gsummptf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptf1o.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsummptf1o.i ⊢ ( 𝑥 = 𝐸 → 𝐶 = 𝐻 )
gsummptf1o.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptf1o.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsummptf1o.d ⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
gsummptf1o.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐹 )
gsummptf1o.e ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐸 ∈ 𝐴 )
gsummptf1o.h ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
Assertion gsummptf1o ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptf1o.x ⊢ Ⅎ 𝑥 𝐻
2 gsummptf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 gsummptf1o.z ⊢ 0 = ( 0g ‘ 𝐺 )
4 gsummptf1o.i ⊢ ( 𝑥 = 𝐸 → 𝐶 = 𝐻 )
5 gsummptf1o.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
6 gsummptf1o.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
7 gsummptf1o.d ⊢ ( 𝜑 → 𝐹 ⊆ 𝐵 )
8 gsummptf1o.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐹 )
9 gsummptf1o.e ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐸 ∈ 𝐴 )
10 gsummptf1o.h ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
11 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ⊆ 𝐵 )
12 11 8 sseldd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
13 12 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 ⟶ 𝐵 )
14 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
15 3 fvexi ⊢ 0 ∈ V
16 15 a1i ⊢ ( 𝜑 → 0 ∈ V )
17 14 6 12 16 fsuppmptdm ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) finSupp 0 )
18 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐷 𝐸 ∈ 𝐴 )
19 10 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 )
20 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) = ( 𝑦 ∈ 𝐷 ↦ 𝐸 )
21 20 f1ompt ⊢ ( ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) : 𝐷 –1-1-onto→ 𝐴 ↔ ( ∀ 𝑦 ∈ 𝐷 𝐸 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐷 𝑥 = 𝐸 ) )
22 18 19 21 sylanbrc ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) : 𝐷 –1-1-onto→ 𝐴 )
23 2 3 5 6 13 17 22 gsumf1o ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) ) )
24 eqidd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) = ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) )
25 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
26 18 24 25 fmptcos ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) = ( 𝑦 ∈ 𝐷 ↦ ⦋ 𝐸 / 𝑥 ⦌ 𝐶 ) )
27 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐷 )
28 1 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → Ⅎ 𝑥 𝐻 )
29 4 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑥 = 𝐸 ) → 𝐶 = 𝐻 )
30 27 28 9 29 csbiedf ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ⦋ 𝐸 / 𝑥 ⦌ 𝐶 = 𝐻 )
31 30 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ ⦋ 𝐸 / 𝑥 ⦌ 𝐶 ) = ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) )
32 26 31 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) = ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) )
33 32 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∘ ( 𝑦 ∈ 𝐷 ↦ 𝐸 ) ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )
34 23 33 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑦 ∈ 𝐷 ↦ 𝐻 ) ) )