Theorem 0ringprmidl

Description: The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024)

	Ref	Expression
Hypothesis	0ringprmidl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion	0ringprmidl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( PrmIdeal ‘ 𝑅 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0ringprmidl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		prmidlssidl	⊢ ( 𝑅 ∈ Ring → ( PrmIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
3	2	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( PrmIdeal ‘ 𝑅 ) ⊆ ( LIdeal ‘ 𝑅 ) )
4		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5	1 4	0ringidl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( LIdeal ‘ 𝑅 ) = { { ( 0g ‘ 𝑅 ) } } )
6	3 5	sseqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( PrmIdeal ‘ 𝑅 ) ⊆ { { ( 0g ‘ 𝑅 ) } } )
7	6	sselda	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ∈ { { ( 0g ‘ 𝑅 ) } } )
8		elsni	⊢ ( 𝑖 ∈ { { ( 0g ‘ 𝑅 ) } } → 𝑖 = { ( 0g ‘ 𝑅 ) } )
9	7 8	syl	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 = { ( 0g ‘ 𝑅 ) } )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11	1 10	prmidlnr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ≠ 𝐵 )
12	11	adantlr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ≠ 𝐵 )
13	1 4	0ring	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
14	13	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝐵 = { ( 0g ‘ 𝑅 ) } )
15	12 14	neeqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑖 ≠ { ( 0g ‘ 𝑅 ) } )
16	15	neneqd	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) → ¬ 𝑖 = { ( 0g ‘ 𝑅 ) } )
17	9 16	pm2.65da	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ¬ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
18	17	eq0rdv	⊢ ( ( 𝑅 ∈ Ring ∧ ( ♯ ‘ 𝐵 ) = 1 ) → ( PrmIdeal ‘ 𝑅 ) = ∅ )