Metamath Proof Explorer

Theorem rprmval

Description: The prime elements of a ring R . (Contributed by Thierry Arnoux, 1-Jul-2024)

Ref Expression
Hypotheses rprmval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
rprmval.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
rprmval.1 ⊢ 0 = ( 0g ‘ 𝑅 )
rprmval.m ⊢ · = ( .r ‘ 𝑅 )
rprmval.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion rprmval ( 𝑅 ∈ 𝑉 → ( RPrime ‘ 𝑅 ) = { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } )

Proof

Step Hyp Ref Expression
1 rprmval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 rprmval.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 rprmval.1 ⊢ 0 = ( 0g ‘ 𝑅 )
4 rprmval.m ⊢ · = ( .r ‘ 𝑅 )
5 rprmval.d ⊢ ∥ = ( ∥r ‘ 𝑅 )
6 df-rprm ⊢ RPrime = ( 𝑟 ∈ V ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑟 ) ∪ { ( 0g ‘ 𝑟 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑟 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) } )
7 fvexd ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V )
8 simpr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → 𝑏 = ( Base ‘ 𝑟 ) )
9 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
10 9 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
11 8 10 eqtrd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → 𝑏 = ( Base ‘ 𝑅 ) )
12 11 1 eqtr4di ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → 𝑏 = 𝐵 )
13 fveq2 ⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
14 13 2 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( Unit ‘ 𝑟 ) = 𝑈 )
15 fveq2 ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
16 15 3 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
17 16 sneqd ⊢ ( 𝑟 = 𝑅 → { ( 0g ‘ 𝑟 ) } = { 0 } )
18 14 17 uneq12d ⊢ ( 𝑟 = 𝑅 → ( ( Unit ‘ 𝑟 ) ∪ { ( 0g ‘ 𝑟 ) } ) = ( 𝑈 ∪ { 0 } ) )
19 18 adantr ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( ( Unit ‘ 𝑟 ) ∪ { ( 0g ‘ 𝑟 ) } ) = ( 𝑈 ∪ { 0 } ) )
20 12 19 difeq12d ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑏 ∖ ( ( Unit ‘ 𝑟 ) ∪ { ( 0g ‘ 𝑟 ) } ) ) = ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) )
21 fvexd ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( ∥r ‘ 𝑟 ) ∈ V )
22 eqidd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → 𝑝 = 𝑝 )
23 simpr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → 𝑑 = ( ∥r ‘ 𝑟 ) )
24 fveq2 ⊢ ( 𝑟 = 𝑅 → ( ∥r ‘ 𝑟 ) = ( ∥r ‘ 𝑅 ) )
25 24 ad2antrr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( ∥r ‘ 𝑟 ) = ( ∥r ‘ 𝑅 ) )
26 23 25 eqtrd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → 𝑑 = ( ∥r ‘ 𝑅 ) )
27 26 5 eqtr4di ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → 𝑑 = ∥ )
28 fveq2 ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
29 28 4 eqtr4di ⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
30 29 ad2antrr ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( .r ‘ 𝑟 ) = · )
31 30 oveqd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
32 22 27 31 breq123d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ↔ 𝑝 ∥ ( 𝑥 · 𝑦 ) ) )
33 27 breqd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( 𝑝 𝑑 𝑥 ↔ 𝑝 ∥ 𝑥 ) )
34 27 breqd ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( 𝑝 𝑑 𝑦 ↔ 𝑝 ∥ 𝑦 ) )
35 33 34 orbi12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ↔ ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) )
36 32 35 imbi12d ⊢ ( ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) ∧ 𝑑 = ( ∥r ‘ 𝑟 ) ) → ( ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) ↔ ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) ) )
37 21 36 sbcied ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( [ ( ∥r ‘ 𝑟 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) ↔ ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) ) )
38 12 37 raleqbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑟 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) ) )
39 12 38 raleqbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑟 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) ) )
40 20 39 rabeqbidv ⊢ ( ( 𝑟 = 𝑅 ∧ 𝑏 = ( Base ‘ 𝑟 ) ) → { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑟 ) ∪ { ( 0g ‘ 𝑟 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑟 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) } = { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } )
41 7 40 csbied ⊢ ( 𝑟 = 𝑅 → ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑝 ∈ ( 𝑏 ∖ ( ( Unit ‘ 𝑟 ) ∪ { ( 0g ‘ 𝑟 ) } ) ) ∣ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 [ ( ∥r ‘ 𝑟 ) / 𝑑 ] ( 𝑝 𝑑 ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) → ( 𝑝 𝑑 𝑥 ∨ 𝑝 𝑑 𝑦 ) ) } = { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } )
42 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
43 1 fvexi ⊢ 𝐵 ∈ V
44 43 difexi ⊢ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∈ V
45 44 rabex ⊢ { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } ∈ V
46 45 a1i ⊢ ( 𝑅 ∈ 𝑉 → { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } ∈ V )
47 6 41 42 46 fvmptd3 ⊢ ( 𝑅 ∈ 𝑉 → ( RPrime ‘ 𝑅 ) = { 𝑝 ∈ ( 𝐵 ∖ ( 𝑈 ∪ { 0 } ) ) ∣ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑝 ∥ ( 𝑥 · 𝑦 ) → ( 𝑝 ∥ 𝑥 ∨ 𝑝 ∥ 𝑦 ) ) } )