Theorem gsum0

Description: Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypothesis	gsum0.z	⊢ 0 = ( 0g ‘ 𝐺 )
Assertion	gsum0	⊢ ( 𝐺 Σg ∅ ) = 0

Proof

Step	Hyp	Ref	Expression
1		gsum0.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4		eqid	⊢ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } = { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) }
5		id	⊢ ( 𝐺 ∈ V → 𝐺 ∈ V )
6		0ex	⊢ ∅ ∈ V
7	6	a1i	⊢ ( 𝐺 ∈ V → ∅ ∈ V )
8		f0	⊢ ∅ : ∅ ⟶ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) }
9	8	a1i	⊢ ( 𝐺 ∈ V → ∅ : ∅ ⟶ { 𝑥 ∈ ( Base ‘ 𝐺 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑦 ) } )
10	2 1 3 4 5 7 9	gsumval1	⊢ ( 𝐺 ∈ V → ( 𝐺 Σg ∅ ) = 0 )
11		df-gsum	⊢ Σg = ( 𝑤 ∈ V , 𝑓 ∈ V ↦ ⦋ { 𝑥 ∈ ( Base ‘ 𝑤 ) ∣ ∀ 𝑦 ∈ ( Base ‘ 𝑤 ) ( ( 𝑥 ( +g ‘ 𝑤 ) 𝑦 ) = 𝑦 ∧ ( 𝑦 ( +g ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } / 𝑜 ⦌ if ( ran 𝑓 ⊆ 𝑜 , ( 0g ‘ 𝑤 ) , if ( dom 𝑓 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( dom 𝑓 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( ( +g ‘ 𝑤 ) , 𝑓 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑔 [ ( ◡ 𝑓 “ ( V ∖ 𝑜 ) ) / 𝑦 ] ( 𝑔 : ( 1 ... ( ♯ ‘ 𝑦 ) ) –1-1-onto→ 𝑦 ∧ 𝑥 = ( seq 1 ( ( +g ‘ 𝑤 ) , ( 𝑓 ∘ 𝑔 ) ) ‘ ( ♯ ‘ 𝑦 ) ) ) ) ) ) )
12	11	reldmmpo	⊢ Rel dom Σg
13	12	ovprc1	⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 Σg ∅ ) = ∅ )
14		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( 0g ‘ 𝐺 ) = ∅ )
15	1 14	syl5eq	⊢ ( ¬ 𝐺 ∈ V → 0 = ∅ )
16	13 15	eqtr4d	⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 Σg ∅ ) = 0 )
17	10 16	pm2.61i	⊢ ( 𝐺 Σg ∅ ) = 0