Theorem subrgcccrng1

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

	Ref	Expression
Hypotheses	subrgcccrng.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
	subrgcccrng.s	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	subrgcccrng1	$$⊢1=1_R$$

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	$$⊢R={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}S$$
2		subrgcccrng.s	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
3		cnfld1	$$⊢1=1_{{ℂ}_{\mathrm{fld}}}$$
4	1 3	subrg1	$$⊢S\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to 1=1_R$$
5	2 4	ax-mp	$$⊢1=1_R$$