Theorem subrgccdom

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

	Ref	Expression
Hypotheses	subrgcccrng.r	|- R = ( CCfld |`s S )
	subrgcccrng.s	|- S e. ( SubRing ` CCfld )
Assertion	subrgccdom	|- R e. Domn

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	|- R = ( CCfld |`s S )
2		subrgcccrng.s	|- S e. ( SubRing ` CCfld )
3	1 2	subrgccnzr	|- R e. NzRing
4		subrgccsscc	|- ( S e. ( SubRing ` CCfld ) -> S C_ CC )
5	2 4	ax-mp	|- S C_ CC
6	5	sseli	|- ( x e. S -> x e. CC )
7	5	sseli	|- ( y e. S -> y e. CC )
8		mul0or	|- ( ( x e. CC /\ y e. CC ) -> ( ( x x. y ) = 0 <-> ( x = 0 \/ y = 0 ) ) )
9	6 7 8	syl2an	|- ( ( x e. S /\ y e. S ) -> ( ( x x. y ) = 0 <-> ( x = 0 \/ y = 0 ) ) )
10	9	biimpd	|- ( ( x e. S /\ y e. S ) -> ( ( x x. y ) = 0 -> ( x = 0 \/ y = 0 ) ) )
11	10	rgen2	|- A. x e. S A. y e. S ( ( x x. y ) = 0 -> ( x = 0 \/ y = 0 ) )
12	1	cnfldsrngbas	|- ( S C_ CC -> S = ( Base ` R ) )
13	5 12	ax-mp	|- S = ( Base ` R )
14		eqid	|- ( CCfld |`s S ) = ( CCfld |`s S )
15	14	cnfldsrngmul	|- ( S e. ( SubRing ` CCfld ) -> x. = ( .r ` ( CCfld |`s S ) ) )
16	2 15	ax-mp	|- x. = ( .r ` ( CCfld |`s S ) )
17	1	fveq2i	|- ( .r ` R ) = ( .r ` ( CCfld |`s S ) )
18	16 17	eqtr4i	|- x. = ( .r ` R )
19	1 2	subrgcccrng0	|- 0 = ( 0g ` R )
20	13 18 19	isdomn	|- ( R e. Domn <-> ( R e. NzRing /\ A. x e. S A. y e. S ( ( x x. y ) = 0 -> ( x = 0 \/ y = 0 ) ) ) )
21	3 11 20	mpbir2an	|- R e. Domn