This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝐺 ∈ V → 0 = ∅ )
16 13 15 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → ( 𝐺 Σg ∅ ) = 0 )
17 10 16 pm2.61i ⊢ ( 𝐺 Σg ∅ ) = 0