Theorem gsumval

Description: Expand out the substitutions in df-gsum . (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	gsumval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumval.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsumval.p	⊢ + = ( +g ‘ 𝐺 )
	gsumval.o	⊢ 𝑂 = { 𝑠 ∈ 𝐵 ∣ ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) }
	gsumval.w	⊢ ( 𝜑 → 𝑊 = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
	gsumval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
	gsumval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	gsumval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	gsumval	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsumval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsumval.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsumval.p	⊢ + = ( +g ‘ 𝐺 )
4		gsumval.o	⊢ 𝑂 = { 𝑠 ∈ 𝐵 ∣ ∀ 𝑡 ∈ 𝐵 ( ( 𝑠 + 𝑡 ) = 𝑡 ∧ ( 𝑡 + 𝑠 ) = 𝑡 ) }
5		gsumval.w	⊢ ( 𝜑 → 𝑊 = ( ◡ 𝐹 “ ( V ∖ 𝑂 ) ) )
6		gsumval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
7		gsumval.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		gsumval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9	1	fvexi	⊢ 𝐵 ∈ V
10	9	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
11		fex2	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
12	8 7 10 11	syl3anc	⊢ ( 𝜑 → 𝐹 ∈ V )
13	8	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
14	1 2 3 4 5 6 12 13	gsumvalx	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = if ( ran 𝐹 ⊆ 𝑂 , 0 , if ( 𝐴 ∈ ran ... , ( ℩ 𝑥 ∃ 𝑚 ∃ 𝑛 ∈ ( ℤ≥ ‘ 𝑚 ) ( 𝐴 = ( 𝑚 ... 𝑛 ) ∧ 𝑥 = ( seq 𝑚 ( + , 𝐹 ) ‘ 𝑛 ) ) ) , ( ℩ 𝑥 ∃ 𝑓 ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑊 ) ) –1-1-onto→ 𝑊 ∧ 𝑥 = ( seq 1 ( + , ( 𝐹 ∘ 𝑓 ) ) ‘ ( ♯ ‘ 𝑊 ) ) ) ) ) ) )