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

Metamath Proof Explorer

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 )