Theorem fsumcnsrcl

Description: Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014)

	Ref	Expression
Hypotheses	fsumcnsrcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
	fsumcnsrcl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumcnsrcl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
Assertion	fsumcnsrcl	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		fsumcnsrcl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ ℂfld ) )
2		fsumcnsrcl.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fsumcnsrcl.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑆 )
4		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
5	4	subrgss	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )
6	1 5	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
7		cnfldadd	⊢ + = ( +g ‘ ℂfld )
8	7	subrgacl	⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 + 𝑏 ) ∈ 𝑆 )
9	8	3expb	⊢ ( ( 𝑆 ∈ ( SubRing ‘ ℂfld ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝑆 )
10	1 9	sylan	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝑆 )
11		subrgsubg	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ∈ ( SubGrp ‘ ℂfld ) )
12		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
13	12	subg0cl	⊢ ( 𝑆 ∈ ( SubGrp ‘ ℂfld ) → 0 ∈ 𝑆 )
14	1 11 13	3syl	⊢ ( 𝜑 → 0 ∈ 𝑆 )
15	6 10 2 3 14	fsumcllem	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ 𝑆 )