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