Theorem gsumval1

Description: Value of the group sum operation when every element being summed is an identity of G . (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumval1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumval1.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumval1.p	⊢ + = ( +g ‘ 𝐺 )
	gsumval1.o	⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
	gsumval1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	gsumval1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
	gsumval1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑂 )
Assertion	gsumval1	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		gsumval1.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumval1.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumval1.p	⊢ + = ( +g ‘ 𝐺 )
4		gsumval1.o	⊢ 𝑂 = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) }
5		gsumval1.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
6		gsumval1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
7		gsumval1.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑂 )
8		eqidd	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
9	4	ssrab3	⊢ 𝑂 ⊆ 𝐵
10		fss	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑂 ∧ 𝑂 ⊆ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
11	7 9 10	sylancl	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
12	1 2 3 4 8 5 6 11	gsumval	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) ) )
13		frn	⊢ ( 𝐹 : 𝐴 ⟶ 𝑂 → ran 𝐹 ⊆ 𝑂 )
14		iftrue	⊢ ( ran 𝐹 ⊆ 𝑂 → if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) ) = 0 )
15	7 13 14	3syl	⊢ ( 𝜑 → if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑧 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑧 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑧 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) –1-1-onto→ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ∧ 𝑧 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) ) ) ) ) ) ) = 0 )
16	12 15	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 0 )