Theorem qsidom

Description: An ideal I in the commutative ring R is prime if and only if the factor ring Q is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024)

	Ref	Expression
Hypothesis	qsidom.1	|- Q = ( R /s ( R ~QG I ) )
Assertion	qsidom	|- ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) )

Proof

Step	Hyp	Ref	Expression
1		qsidom.1	|- Q = ( R /s ( R ~QG I ) )
2	1	qsidomlem1	|- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) )
3	1	qsidomlem2	|- ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn )
4	3	adantlr	|- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn )
5	2 4	impbida	|- ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) )