Metamath Proof Explorer


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 / 𝑠 R ~ QG I
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 / 𝑠 R ~ QG I
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 |-