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 𝐹 ) = ⦋ 𝑋 / 𝑛 ⦌ 𝐴 )