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

Metamath Proof Explorer

Theorem gsummpt1n0

Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 . (Contributed by AV, 11-Oct-2019)

Ref Expression
Hypotheses gsummpt1n0.0 ⊢ 0 = ( 0g ‘ 𝐺 )
gsummpt1n0.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsummpt1n0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
gsummpt1n0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
gsummpt1n0.f ⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
gsummpt1n0.a ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐼 𝐴 ∈ ( Base ‘ 𝐺 ) )
Assertion gsummpt1n0 ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )

Proof

Step Hyp Ref Expression
1 gsummpt1n0.0 ⊢ 0 = ( 0g ‘ 𝐺 )
2 gsummpt1n0.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3 gsummpt1n0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
4 gsummpt1n0.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
5 gsummpt1n0.f ⊢ 𝐹 = ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
6 gsummpt1n0.a ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝐼 𝐴 ∈ ( Base ‘ 𝐺 ) )
7 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
8 6 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 𝐴 ∈ ( Base ‘ 𝐺 ) )
9 7 1 mndidcl ⊢ ( 𝐺 ∈ Mnd → 0 ∈ ( Base ‘ 𝐺 ) )
10 2 9 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐺 ) )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → 0 ∈ ( Base ‘ 𝐺 ) )
12 8 11 ifcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐼 ) → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ∈ ( Base ‘ 𝐺 ) )
13 12 5 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
14 5 oveq1i ⊢ ( 𝐹 supp 0 ) = ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) supp 0 )
15 eldifsni ⊢ ( 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) → 𝑛 ≠ 𝑋 )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → 𝑛 ≠ 𝑋 )
17 ifnefalse ⊢ ( 𝑛 ≠ 𝑋 → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 0 )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐼 ∖ { 𝑋 } ) ) → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = 0 )
19 18 3 suppss2 ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) supp 0 ) ⊆ { 𝑋 } )
20 14 19 eqsstrid ⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ { 𝑋 } )
21 7 1 2 3 4 13 20 gsumpt ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐹 ‘ 𝑋 ) )
22 nfcv ⊢ Ⅎ 𝑦 if ( 𝑛 = 𝑋 , 𝐴 , 0 )
23 nfv ⊢ Ⅎ 𝑛 𝑦 = 𝑋
24 nfcsb1v ⊢ Ⅎ 𝑛 ⦋ 𝑦 / 𝑛 ⦌ 𝐴
25 nfcv ⊢ Ⅎ 𝑛 0
26 23 24 25 nfif ⊢ Ⅎ 𝑛 if ( 𝑦 = 𝑋 , ⦋ 𝑦 / 𝑛 ⦌ 𝐴 , 0 )
27 eqeq1 ⊢ ( 𝑛 = 𝑦 → ( 𝑛 = 𝑋 ↔ 𝑦 = 𝑋 ) )
28 csbeq1a ⊢ ( 𝑛 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑛 ⦌ 𝐴 )
29 27 28 ifbieq1d ⊢ ( 𝑛 = 𝑦 → if ( 𝑛 = 𝑋 , 𝐴 , 0 ) = if ( 𝑦 = 𝑋 , ⦋ 𝑦 / 𝑛 ⦌ 𝐴 , 0 ) )
30 22 26 29 cbvmpt ⊢ ( 𝑛 ∈ 𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) ) = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , ⦋ 𝑦 / 𝑛 ⦌ 𝐴 , 0 ) )
31 5 30 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝐼 ↦ if ( 𝑦 = 𝑋 , ⦋ 𝑦 / 𝑛 ⦌ 𝐴 , 0 ) )
32 iftrue ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑋 , ⦋ 𝑦 / 𝑛 ⦌ 𝐴 , 0 ) = ⦋ 𝑦 / 𝑛 ⦌ 𝐴 )
33 csbeq1 ⊢ ( 𝑦 = 𝑋 → ⦋ 𝑦 / 𝑛 ⦌ 𝐴 = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )
34 32 33 eqtrd ⊢ ( 𝑦 = 𝑋 → if ( 𝑦 = 𝑋 , ⦋ 𝑦 / 𝑛 ⦌ 𝐴 , 0 ) = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )
35 rspcsbela ⊢ ( ( 𝑋 ∈ 𝐼 ∧ ∀ 𝑛 ∈ 𝐼 𝐴 ∈ ( Base ‘ 𝐺 ) ) → ⦋ 𝑋 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝐺 ) )
36 4 6 35 syl2anc ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑛 ⦌ 𝐴 ∈ ( Base ‘ 𝐺 ) )
37 31 34 4 36 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )
38 21 37 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )