Theorem subrgcccrng1

Description: The one of a subring of the complex numbers. (Contributed by AV, 26-Oct-2026)

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

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
2		subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
3		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
4	1 3	subrg1	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 1 = ( 1r ‘ 𝑅 ) )
5	2 4	ax-mp	⊢ 1 = ( 1r ‘ 𝑅 )