Theorem gsumunsnfd

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 11-Dec-2019)

	Ref	Expression
Hypotheses	gsumunsnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumunsnd.p	⊢ + = ( +g ‘ 𝐺 )
	gsumunsnd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumunsnd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsumunsnd.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
	gsumunsnd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
	gsumunsnd.d	⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
	gsumunsnd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	gsumunsnd.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
	gsumunsnfd.0	⊢ Ⅎ 𝑘 𝑌
Assertion	gsumunsnfd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumunsnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumunsnd.p	⊢ + = ( +g ‘ 𝐺 )
3		gsumunsnd.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsumunsnd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		gsumunsnd.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
6		gsumunsnd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
7		gsumunsnd.d	⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
8		gsumunsnd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		gsumunsnd.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
10		gsumunsnfd.0	⊢ Ⅎ 𝑘 𝑌
11		snfi	⊢ { 𝑀 } ∈ Fin
12		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑀 } ∈ Fin ) → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
13	4 11 12	sylancl	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
14		elun	⊢ ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) )
15		elsni	⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
16	15 9	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑋 = 𝑌 )
17	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑌 ∈ 𝐵 )
18	16 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑋 ∈ 𝐵 )
19	5 18	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
20	14 19	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
21		disjsn	⊢ ( ( 𝐴 ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ 𝐴 )
22	7 21	sylibr	⊢ ( 𝜑 → ( 𝐴 ∩ { 𝑀 } ) = ∅ )
23		eqidd	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) = ( 𝐴 ∪ { 𝑀 } ) )
24	1 2 3 13 20 22 23	gsummptfidmsplit	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) )
25		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
26	3 25	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
27		nfv	⊢ Ⅎ 𝑘 𝜑
28	1 26 6 8 9 27 10	gsumsnfd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) = 𝑌 )
29	28	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )
30	24 29	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )