Theorem subrgcccrng0

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

	Ref	Expression
Hypotheses	subrgcccrng.r	|- R = ( CCfld |`s S )
	subrgcccrng.s	|- S e. ( SubRing ` CCfld )
Assertion	subrgcccrng0	|- 0 = ( 0g ` R )

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	|- R = ( CCfld |`s S )
2		subrgcccrng.s	|- S e. ( SubRing ` CCfld )
3		cnfld0	|- 0 = ( 0g ` CCfld )
4	1 3	subrg0	|- ( S e. ( SubRing ` CCfld ) -> 0 = ( 0g ` R ) )
5	2 4	ax-mp	|- 0 = ( 0g ` R )