Theorem isrprm

Description: Property for P to be a prime element in the ring R . (Contributed by Thierry Arnoux, 1-Jul-2024)

	Ref	Expression
Hypotheses	isrprm.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	isrprm.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
	isrprm.3	⊢ 0 = ( 0g ‘ 𝑅 )
	isrprm.4	⊢ ∥ = ( ∥r ‘ 𝑅 )
	isrprm.5	⊢ · = ( .r ‘ 𝑅 )
Assertion	isrprm	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑃 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isrprm.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		isrprm.2	⊢ 𝑈 = ( Unit ‘ 𝑅 )
3		isrprm.3	⊢ 0 = ( 0g ‘ 𝑅 )
4		isrprm.4	⊢ ∥ = ( ∥r ‘ 𝑅 )
5		isrprm.5	⊢ · = ( .r ‘ 𝑅 )
6	1 2 3 5 4	rprmval	⊢ ( 𝑅 ∈ 𝑉 → ( RPrime ‘ 𝑅 ) = { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } )
7	6	eleq2d	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑃 ∈ ( RPrime ‘ 𝑅 ) ↔ 𝑃 ∈ { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } ) )
8		breq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∥ ( 𝑥 · 𝑦 ) ↔ 𝑃 ∥ ( 𝑥 · 𝑦 ) ) )
9		breq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∥ 𝑥 ↔ 𝑃 ∥ 𝑥 ) )
10		breq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∥ 𝑦 ↔ 𝑃 ∥ 𝑦 ) )
11	9 10	orbi12d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ↔ ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) )
12	8 11	imbi12d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) ↔ ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) )
13	12	2ralbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) )
14	13	elrab	⊢ ( 𝑃 ∈ { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } ↔ ( 𝑃 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) )
15	7 14	bitrdi	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑃 ∈ ( RPrime ‘ 𝑅 ) ↔ ( 𝑃 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑃 ∥ ( 𝑥 · 𝑦 ) → ( 𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦 ) ) ) ) )