Theorem subrgccdom

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

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

Proof

Step	Hyp	Ref	Expression
1		subrgcccrng.r	⊢ 𝑅 = ( ℂfld ↾s 𝑆 )
2		subrgcccrng.s	⊢ 𝑆 ∈ ( SubRing ‘ ℂfld )
3	1 2	subrgccnzr	⊢ 𝑅 ∈ NzRing
4		subrgccsscc	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → 𝑆 ⊆ ℂ )
5	2 4	ax-mp	⊢ 𝑆 ⊆ ℂ
6	5	sseli	⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ℂ )
7	5	sseli	⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ℂ )
8		mul0or	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) = 0 ↔ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
9	6 7 8	syl2an	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 · 𝑦 ) = 0 ↔ ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
10	9	biimpd	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) )
11	10	rgen2	⊢ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) )
12	1	cnfldsrngbas	⊢ ( 𝑆 ⊆ ℂ → 𝑆 = ( Base ‘ 𝑅 ) )
13	5 12	ax-mp	⊢ 𝑆 = ( Base ‘ 𝑅 )
14		eqid	⊢ ( ℂfld ↾s 𝑆 ) = ( ℂfld ↾s 𝑆 )
15	14	cnfldsrngmul	⊢ ( 𝑆 ∈ ( SubRing ‘ ℂfld ) → · = ( .r ‘ ( ℂfld ↾s 𝑆 ) ) )
16	2 15	ax-mp	⊢ · = ( .r ‘ ( ℂfld ↾s 𝑆 ) )
17	1	fveq2i	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ ( ℂfld ↾s 𝑆 ) )
18	16 17	eqtr4i	⊢ · = ( .r ‘ 𝑅 )
19	1 2	subrgcccrng0	⊢ 0 = ( 0g ‘ 𝑅 )
20	13 18 19	isdomn	⊢ ( 𝑅 ∈ Domn ↔ ( 𝑅 ∈ NzRing ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 · 𝑦 ) = 0 → ( 𝑥 = 0 ∨ 𝑦 = 0 ) ) ) )
21	3 11 20	mpbir2an	⊢ 𝑅 ∈ Domn