Theorem gsumzresunsn

Description: Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023)

	Ref	Expression
Hypotheses	gsumzresunsn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumzresunsn.p	⊢ + = ( +g ‘ 𝐺 )
	gsumzresunsn.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	gsumzresunsn.y	⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
	gsumzresunsn.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
	gsumzresunsn.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
	gsumzresunsn.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
	gsumzresunsn.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsumzresunsn.2	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
	gsumzresunsn.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
	gsumzresunsn.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	gsumzresunsn.5	⊢ ( 𝜑 → ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ) )
Assertion	gsumzresunsn	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumzresunsn.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumzresunsn.p	⊢ + = ( +g ‘ 𝐺 )
3		gsumzresunsn.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		gsumzresunsn.y	⊢ 𝑌 = ( 𝐹 ‘ 𝑋 )
5		gsumzresunsn.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐵 )
6		gsumzresunsn.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
7		gsumzresunsn.g	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
8		gsumzresunsn.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
9		gsumzresunsn.2	⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
10		gsumzresunsn.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
11		gsumzresunsn.4	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
12		gsumzresunsn.5	⊢ ( 𝜑 → ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ⊆ ( 𝑍 ‘ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ) )
13		eqid	⊢ ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) )
14		df-ima	⊢ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) = ran ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) )
15	10	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐶 )
16	6 15	unssd	⊢ ( 𝜑 → ( 𝐴 ∪ { 𝑋 } ) ⊆ 𝐶 )
17	5 16	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) = ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
18	17	rneqd	⊢ ( 𝜑 → ran ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) = ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
19	14 18	syl5eq	⊢ ( 𝜑 → ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) = ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
20	19	fveq2d	⊢ ( 𝜑 → ( 𝑍 ‘ ( 𝐹 “ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( 𝑍 ‘ ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
21	12 19 20	3sstr3d	⊢ ( 𝜑 → ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝑍 ‘ ran ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
22	5	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐹 : 𝐶 ⟶ 𝐵 )
23	6	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐶 )
24	22 23	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
26	25	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
27	26 4	eqtr4di	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = 𝑌 )
28	1 2 3 13 7 8 21 24 10 9 11 27	gsumzunsnd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) + 𝑌 ) )
29	17	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∪ { 𝑋 } ) ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
30	5 6	feqresmpt	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
31	30	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
32	31	oveq1d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + 𝑌 ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) ) + 𝑌 ) )
33	28 29 32	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐹 ↾ ( 𝐴 ∪ { 𝑋 } ) ) ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐴 ) ) + 𝑌 ) )