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

Metamath Proof Explorer

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 ‘ 𝑅 ) = ∅ )