Metamath Proof Explorer


Theorem pridln1

Description: A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024)

Ref Expression
Hypotheses pridln1.1 𝐵 = ( Base ‘ 𝑅 )
pridln1.2 1 = ( 1r𝑅 )
Assertion pridln1 ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼𝐵 ) → ¬ 1𝐼 )

Proof

Step Hyp Ref Expression
1 pridln1.1 𝐵 = ( Base ‘ 𝑅 )
2 pridln1.2 1 = ( 1r𝑅 )
3 eqid ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
4 3 1 2 lidl1el ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 1𝐼𝐼 = 𝐵 ) )
5 4 necon3bbid ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ) → ( ¬ 1𝐼𝐼𝐵 ) )
6 5 biimp3ar ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼𝐵 ) → ¬ 1𝐼 )