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 ∈ 𝐼 ) |
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 ∈ 𝐼 ) |