Theorem subrgcccrng

Description: A subring of the complex numbers is a commutative ring. (Contributed by AV, 26-Oct-2026)

	Ref	Expression
Hypotheses	subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
	subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
Assertion	subrgcccrng	⊢ 𝑅 ∈ CRing

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
2		subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
3		cncrng	⊢ ℂfld ∈ CRing
4	1	subrgcrng	⊢ ( ( ℂfld ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ ℂfld ) ) → 𝑅 ∈ CRing )
5	3 2 4	mp2an	⊢ 𝑅 ∈ CRing