drngmxidl

Description: The zero ideal is the only ideal of a division ring. (Contributed by Thierry Arnoux, 16-Mar-2025)

		Ref	Expression
	Hypothesis	drngmxidl.1	⊢ 0 = ( 0_g ‘ 𝑅 )
	Assertion	drngmxidl	⊢ ( 𝑅 ∈ DivRing → ( MaxIdeal ‘ 𝑅 ) = { { 0 } } )

Proof

Step	Hyp	Ref	Expression
1		drngmxidl.1	⊢ 0 = ( 0_g ‘ 𝑅 )
2		drngring	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
3		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4	3	mxidlidl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
5	4	ex	⊢ ( 𝑅 ∈ Ring → ( 𝑖 ∈ ( MaxIdeal ‘ 𝑅 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) )
6	5	ssrdv	⊢ ( 𝑅 ∈ Ring → ( MaxIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
7	2 6	syl	⊢ ( 𝑅 ∈ DivRing → ( MaxIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
8		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
9	3 1 8	drngnidl	⊢ ( 𝑅 ∈ DivRing → ( LIdeal ‘ 𝑅 ) = { { 0 } , ( Base ‘ 𝑅 ) } )
10	7 9	sseqtrd	⊢ ( 𝑅 ∈ DivRing → ( MaxIdeal ‘ 𝑅 ) ⊆ { { 0 } , ( Base ‘ 𝑅 ) } )
11	3	mxidlnr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑖 ≠ ( Base ‘ 𝑅 ) )
12	2 11	sylan	⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑖 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑖 ≠ ( Base ‘ 𝑅 ) )
13	12	nelrdva	⊢ ( 𝑅 ∈ DivRing → ¬ ( Base ‘ 𝑅 ) ∈ ( MaxIdeal ‘ 𝑅 ) )
14		ssdifsn	⊢ ( ( MaxIdeal ‘ 𝑅 ) ⊆ ( { { 0 } , ( Base ‘ 𝑅 ) } ∖ { ( Base ‘ 𝑅 ) } ) ↔ ( ( MaxIdeal ‘ 𝑅 ) ⊆ { { 0 } , ( Base ‘ 𝑅 ) } ∧ ¬ ( Base ‘ 𝑅 ) ∈ ( MaxIdeal ‘ 𝑅 ) ) )
15	10 13 14	sylanbrc	⊢ ( 𝑅 ∈ DivRing → ( MaxIdeal ‘ 𝑅 ) ⊆ ( { { 0 } , ( Base ‘ 𝑅 ) } ∖ { ( Base ‘ 𝑅 ) } ) )
16		drngnzr	⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ NzRing )
17	1 3	drnglidl1ne0	⊢ ( 𝑅 ∈ NzRing → ( Base ‘ 𝑅 ) ≠ { 0 } )
18	17	necomd	⊢ ( 𝑅 ∈ NzRing → { 0 } ≠ ( Base ‘ 𝑅 ) )
19		difprsn2	⊢ ( { 0 } ≠ ( Base ‘ 𝑅 ) → ( { { 0 } , ( Base ‘ 𝑅 ) } ∖ { ( Base ‘ 𝑅 ) } ) = { { 0 } } )
20	16 18 19	3syl	⊢ ( 𝑅 ∈ DivRing → ( { { 0 } , ( Base ‘ 𝑅 ) } ∖ { ( Base ‘ 𝑅 ) } ) = { { 0 } } )
21	15 20	sseqtrd	⊢ ( 𝑅 ∈ DivRing → ( MaxIdeal ‘ 𝑅 ) ⊆ { { 0 } } )
22	1	drng0mxidl	⊢ ( 𝑅 ∈ DivRing → { 0 } ∈ ( MaxIdeal ‘ 𝑅 ) )
23	22	snssd	⊢ ( 𝑅 ∈ DivRing → { { 0 } } ⊆ ( MaxIdeal ‘ 𝑅 ) )
24	21 23	eqssd	⊢ ( 𝑅 ∈ DivRing → ( MaxIdeal ‘ 𝑅 ) = { { 0 } } )

Metamath Proof Explorer

Theorem drngmxidl

Proof