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

Metamath Proof Explorer

Theorem gsummptres

Description: Extend a finite group sum by padding outside with zeroes. Proof generated using OpenAI's proof assistant. (Contributed by Thierry Arnoux, 11-Jul-2020)

Ref Expression
Hypotheses gsummptres.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsummptres.1 ⊢ 0 = ( 0g ‘ 𝐺 )
gsummptres.2 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsummptres.3 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsummptres.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
gsummptres.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ) → 𝐶 = 0 )
Assertion gsummptres ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptres.0 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsummptres.1 ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsummptres.2 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4 gsummptres.3 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
5 gsummptres.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
6 gsummptres.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ) → 𝐶 = 0 )
7 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
8 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
9 2 fvexi ⊢ 0 ∈ V
10 9 a1i ⊢ ( 𝜑 → 0 ∈ V )
11 8 4 5 10 fsuppmptdm ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) finSupp 0 )
12 inindif ⊢ ( ( 𝐴 ∩ 𝐷 ) ∩ ( 𝐴 ∖ 𝐷 ) ) = ∅
13 12 a1i ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐷 ) ∩ ( 𝐴 ∖ 𝐷 ) ) = ∅ )
14 inundif ⊢ ( ( 𝐴 ∩ 𝐷 ) ∪ ( 𝐴 ∖ 𝐷 ) ) = 𝐴
15 14 eqcomi ⊢ 𝐴 = ( ( 𝐴 ∩ 𝐷 ) ∪ ( 𝐴 ∖ 𝐷 ) )
16 15 a1i ⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∩ 𝐷 ) ∪ ( 𝐴 ∖ 𝐷 ) ) )
17 1 2 7 3 4 5 11 13 16 gsumsplit2 ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) ) ) )
18 6 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) = ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 0 ) )
19 18 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 0 ) ) )
20 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
21 3 20 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
22 diffi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝐷 ) ∈ Fin )
23 4 22 syl ⊢ ( 𝜑 → ( 𝐴 ∖ 𝐷 ) ∈ Fin )
24 2 gsumz ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 ∖ 𝐷 ) ∈ Fin ) → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 0 ) ) = 0 )
25 21 23 24 syl2anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 0 ) ) = 0 )
26 19 25 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) ) = 0 )
27 26 oveq2d ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ( +g ‘ 𝐺 ) 0 ) )
28 infi ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∩ 𝐷 ) ∈ Fin )
29 4 28 syl ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐷 ) ∈ Fin )
30 inss1 ⊢ ( 𝐴 ∩ 𝐷 ) ⊆ 𝐴
31 30 sseli ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) → 𝑥 ∈ 𝐴 )
32 31 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ) → 𝐶 ∈ 𝐵 )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) 𝐶 ∈ 𝐵 )
34 1 3 29 33 gsummptcl ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ∈ 𝐵 )
35 1 7 2 mndrid ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) )
36 21 34 35 syl2anc ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) )
37 27 36 eqtrd ⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝐷 ) ↦ 𝐶 ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) )
38 17 37 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∩ 𝐷 ) ↦ 𝐶 ) ) )