Theorem rprmnunit

Description: A ring prime is not a unit. (Contributed by Thierry Arnoux, 18-May-2025)

	Ref	Expression
Hypotheses	rprmdvds.2	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
	rprmdvds.3	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	rprmdvds.5	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	rprmdvds.6	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
Assertion	rprmnunit	⊢ ( 𝜑 → ¬ 𝑄 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		rprmdvds.2	⊢ 𝑃 = ( RPrime ‘ 𝑅 )
2		rprmdvds.3	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		rprmdvds.5	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
4		rprmdvds.6	⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
5		eqidd	⊢ ( 𝜑 → ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) = ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) )
6	4 1	eleqtrdi	⊢ ( 𝜑 → 𝑄 ∈ ( RPrime ‘ 𝑅 ) )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
9		eqid	⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
10		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
11	7 2 8 9 10	isrprm	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑄 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑄 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) → ( 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) ) ) ) )
12	11	simprbda	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑄 ∈ ( RPrime ‘ 𝑅 ) ) → 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) ) )
13	3 6 12	syl2anc	⊢ ( 𝜑 → 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) ) )
14	13	eldifbd	⊢ ( 𝜑 → ¬ 𝑄 ∈ ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) )
15		nelun	⊢ ( ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) = ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) → ( ¬ 𝑄 ∈ ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) ↔ ( ¬ 𝑄 ∈ 𝑈 ∧ ¬ 𝑄 ∈ { ( 0g ‘ 𝑅 ) } ) ) )
16	15	simprbda	⊢ ( ( ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) = ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) ∧ ¬ 𝑄 ∈ ( 𝑈 ∪ { ( 0g ‘ 𝑅 ) } ) ) → ¬ 𝑄 ∈ 𝑈 )
17	5 14 16	syl2anc	⊢ ( 𝜑 → ¬ 𝑄 ∈ 𝑈 )