Theorem gsumzunsnd

Description: Append an element to a finite group sum, more general version of gsumunsnd . (Contributed by AV, 7-Oct-2019)

	Ref	Expression
Hypotheses	gsumzunsnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumzunsnd.p	⊢ + = ( +g ‘ 𝐺 )
	gsumzunsnd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	gsumzunsnd.f	⊢ 𝐹 = ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 )
	gsumzunsnd.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	gsumzunsnd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsumzunsnd.c	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
	gsumzunsnd.x	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
	gsumzunsnd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
	gsumzunsnd.d	⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
	gsumzunsnd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	gsumzunsnd.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
Assertion	gsumzunsnd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumzunsnd.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumzunsnd.p	⊢ + = ( +g ‘ 𝐺 )
3		gsumzunsnd.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		gsumzunsnd.f	⊢ 𝐹 = ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 )
5		gsumzunsnd.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
6		gsumzunsnd.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
7		gsumzunsnd.c	⊢ ( 𝜑 → ran 𝐹 ⊆ ( 𝑍 ‘ ran 𝐹 ) )
8		gsumzunsnd.x	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
9		gsumzunsnd.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
10		gsumzunsnd.d	⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
11		gsumzunsnd.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12		gsumzunsnd.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
13		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
14		snfi	⊢ { 𝑀 } ∈ Fin
15		unfi	⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑀 } ∈ Fin ) → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
16	6 14 15	sylancl	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) ∈ Fin )
17		elun	⊢ ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) )
18		elsni	⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
19	18 12	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑋 = 𝑌 )
20	11	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑌 ∈ 𝐵 )
21	19 20	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝑋 ∈ 𝐵 )
22	8 21	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
23	17 22	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
24	23 4	fmptd	⊢ ( 𝜑 → 𝐹 : ( 𝐴 ∪ { 𝑀 } ) ⟶ 𝐵 )
25	8	expcom	⊢ ( 𝑘 ∈ 𝐴 → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
26	11	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑌 ∈ 𝐵 )
27	12 26	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 ∈ 𝐵 )
28	27	expcom	⊢ ( 𝑘 = 𝑀 → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
29	18 28	syl	⊢ ( 𝑘 ∈ { 𝑀 } → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
30	25 29	jaoi	⊢ ( ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ { 𝑀 } ) → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
31	17 30	sylbi	⊢ ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) → ( 𝜑 → 𝑋 ∈ 𝐵 ) )
32	31	impcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ) → 𝑋 ∈ 𝐵 )
33		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
34	4 16 32 33	fsuppmptdm	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) )
35		disjsn	⊢ ( ( 𝐴 ∩ { 𝑀 } ) = ∅ ↔ ¬ 𝑀 ∈ 𝐴 )
36	10 35	sylibr	⊢ ( 𝜑 → ( 𝐴 ∩ { 𝑀 } ) = ∅ )
37		eqidd	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑀 } ) = ( 𝐴 ∪ { 𝑀 } ) )
38	1 13 2 3 5 16 24 7 34 36 37	gsumzsplit	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + ( 𝐺 Σg ( 𝐹 ↾ { 𝑀 } ) ) ) )
39	4	reseq1i	⊢ ( 𝐹 ↾ 𝐴 ) = ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ 𝐴 )
40		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑀 } )
41		resmpt	⊢ ( 𝐴 ⊆ ( 𝐴 ∪ { 𝑀 } ) → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
42	40 41	mp1i	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
43	39 42	eqtrid	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) )
44	43	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) )
45	4	reseq1i	⊢ ( 𝐹 ↾ { 𝑀 } ) = ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ { 𝑀 } )
46		ssun2	⊢ { 𝑀 } ⊆ ( 𝐴 ∪ { 𝑀 } )
47		resmpt	⊢ ( { 𝑀 } ⊆ ( 𝐴 ∪ { 𝑀 } ) → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) )
48	46 47	mp1i	⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) )
49	45 48	eqtrid	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝑀 } ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) )
50	49	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ { 𝑀 } ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) )
51	44 50	oveq12d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + ( 𝐺 Σg ( 𝐹 ↾ { 𝑀 } ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) )
52	1 5 9 11 12	gsumsnd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) = 𝑌 )
53	52	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )
54	38 51 53	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )