This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qsfld

Description: An ideal M in the commutative ring R is maximal if and only if the factor ring Q is a field. (Contributed by Thierry Arnoux, 13-Mar-2025)

Ref Expression
Hypotheses qsfld.1 ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
qsfld.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
qsfld.3 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
qsfld.4 ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
Assertion qsfld ( 𝜑 → ( 𝑄 ∈ Field ↔ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 qsfld.1 ⊢ 𝑄 = ( 𝑅 /s ( 𝑅 ~QG 𝑀 ) )
2 qsfld.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
3 qsfld.3 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
4 qsfld.4 ⊢ ( 𝜑 → 𝑀 ∈ ( LIdeal ‘ 𝑅 ) )
5 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
6 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
7 6 crng2idl ⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
8 2 7 syl ⊢ ( 𝜑 → ( LIdeal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 ) )
9 4 8 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( 2Ideal ‘ 𝑅 ) )
10 5 1 3 9 qsdrng ⊢ ( 𝜑 → ( 𝑄 ∈ DivRing ↔ ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) )
11 isfld ⊢ ( 𝑄 ∈ Field ↔ ( 𝑄 ∈ DivRing ∧ 𝑄 ∈ CRing ) )
12 1 6 quscrng ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑄 ∈ CRing )
13 2 4 12 syl2anc ⊢ ( 𝜑 → 𝑄 ∈ CRing )
14 13 biantrud ⊢ ( 𝜑 → ( 𝑄 ∈ DivRing ↔ ( 𝑄 ∈ DivRing ∧ 𝑄 ∈ CRing ) ) )
15 11 14 bitr4id ⊢ ( 𝜑 → ( 𝑄 ∈ Field ↔ 𝑄 ∈ DivRing ) )
16 eqid ⊢ ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ 𝑅 )
17 16 5 crngmxidl ⊢ ( 𝑅 ∈ CRing → ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) )
18 2 17 syl ⊢ ( 𝜑 → ( MaxIdeal ‘ 𝑅 ) = ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) )
19 18 eleq2d ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
20 19 biimpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) → 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
21 20 pm4.71d ⊢ ( 𝜑 → ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ∧ 𝑀 ∈ ( MaxIdeal ‘ ( oppr ‘ 𝑅 ) ) ) ) )
22 10 15 21 3bitr4d ⊢ ( 𝜑 → ( 𝑄 ∈ Field ↔ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) )