Metamath Proof Explorer

Theorem crngmxidl

Description: In a commutative ring, maximal ideals of the opposite ring coincide with maximal ideals. (Contributed by Thierry Arnoux, 13-Mar-2025)

		Ref	Expression
	Hypotheses	crngmxidl.i	⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
		crngmxidl.o	⊢ 𝑂 = ( opp_r ‘ 𝑅 )
	Assertion	crngmxidl	⊢ ( 𝑅 ∈ CRing → 𝑀 = ( MaxIdeal ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		crngmxidl.i	⊢ 𝑀 = ( MaxIdeal ‘ 𝑅 )
2		crngmxidl.o	⊢ 𝑂 = ( opp_r ‘ 𝑅 )
3	1	eleq2i	⊢ ( 𝑚 ∈ 𝑀 ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) )
4		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
5	4 2	crngridl	⊢ ( 𝑅 ∈ CRing → ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑂 ) )
6	5	eleq2d	⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ↔ 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ) )
7	5	raleqdv	⊢ ( 𝑅 ∈ CRing → ( ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ↔ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) )
8	6 7	3anbi13d	⊢ ( 𝑅 ∈ CRing → ( ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
9		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11	10	ismxidl	⊢ ( 𝑅 ∈ Ring → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
12	9 11	syl	⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
13	2	opprring	⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
14	2 10	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
15	14	ismxidl	⊢ ( 𝑂 ∈ Ring → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
16	9 13 15	3syl	⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ↔ ( 𝑚 ∈ ( LIdeal ‘ 𝑂 ) ∧ 𝑚 ≠ ( Base ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ ( LIdeal ‘ 𝑂 ) ( 𝑚 ⊆ 𝑗 → ( 𝑗 = 𝑚 ∨ 𝑗 = ( Base ‘ 𝑅 ) ) ) ) ) )
17	8 12 16	3bitr4d	⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ ( MaxIdeal ‘ 𝑅 ) ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ) )
18	3 17	bitrid	⊢ ( 𝑅 ∈ CRing → ( 𝑚 ∈ 𝑀 ↔ 𝑚 ∈ ( MaxIdeal ‘ 𝑂 ) ) )
19	18	eqrdv	⊢ ( 𝑅 ∈ CRing → 𝑀 = ( MaxIdeal ‘ 𝑂 ) )