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{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
Assertion	qsidom	Could not format assertion : No typesetting found for |- ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		qsidom.1	$$⊢Q=R{/}_{𝑠}\left(R{~}_{\mathit{QG}}I\right)$$
2	1	qsidomlem1	Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) with typecode |-
3	1	qsidomlem2	Could not format ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) : No typesetting found for |- ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) with typecode |-
4	3	adantlr	Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) with typecode |-
5	2 4	impbida	Could not format ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) ) with typecode |-