Metamath Proof Explorer

Theorem rprmirred

Description: In an integral domain, ring primes are irreducible. (Contributed by Thierry Arnoux, 18-May-2025)

Ref Expression
Hypotheses rprmirred.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
rprmirred.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
rprmirred.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
rprmirred.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
Assertion rprmirred ( 𝜑 → 𝑄 ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 rprmirred.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
2 rprmirred.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
3 rprmirred.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑃 )
4 rprmirred.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 5 1 4 3 rprmcl ⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝑅 ) )
7 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
8 1 7 4 3 rprmnunit ⊢ ( 𝜑 → ¬ 𝑄 ∈ ( Unit ‘ 𝑅 ) )
9 6 8 eldifd ⊢ ( 𝜑 → 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
10 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
13 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑅 ∈ IDomn )
14 13 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑅 ∈ IDomn )
15 1 10 4 3 rprmnz ⊢ ( 𝜑 → 𝑄 ≠ ( 0g ‘ 𝑅 ) )
16 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑄 ≠ ( 0g ‘ 𝑅 ) )
17 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
18 17 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
20 19 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
21 20 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
22 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 )
23 22 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑄 = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
24 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 )
25 5 7 10 11 12 14 16 18 21 23 24 rprmirredlem ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑦 ∈ ( Unit ‘ 𝑅 ) )
26 19 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
27 26 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → ¬ 𝑦 ∈ ( Unit ‘ 𝑅 ) )
28 25 27 pm2.21fal ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ) → ⊥ )
29 13 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑅 ∈ IDomn )
30 15 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑄 ≠ ( 0g ‘ 𝑅 ) )
31 19 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
32 17 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
33 32 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
34 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 )
35 29 idomcringd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑅 ∈ CRing )
36 20 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
37 5 11 35 33 36 crngcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
38 34 37 eqtr3d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑄 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
39 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 )
40 5 7 10 11 12 29 30 31 33 38 39 rprmirredlem ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑥 ∈ ( Unit ‘ 𝑅 ) )
41 17 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
42 41 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → ¬ 𝑥 ∈ ( Unit ‘ 𝑅 ) )
43 40 42 pm2.21fal ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) ∧ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) → ⊥ )
44 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑄 ∈ 𝑃 )
45 4 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
46 5 12 dvdsrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ ( Base ‘ 𝑅 ) ) → 𝑄 ( ∥r ‘ 𝑅 ) 𝑄 )
47 45 6 46 syl2anc ⊢ ( 𝜑 → 𝑄 ( ∥r ‘ 𝑅 ) 𝑄 )
48 47 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑄 ( ∥r ‘ 𝑅 ) 𝑄 )
49 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 )
50 48 49 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → 𝑄 ( ∥r ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
51 5 1 12 11 13 44 32 20 50 rprmdvds ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → ( 𝑄 ( ∥r ‘ 𝑅 ) 𝑥 ∨ 𝑄 ( ∥r ‘ 𝑅 ) 𝑦 ) )
52 28 43 51 mpjaodan ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 ) → ⊥ )
53 52 inegd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → ¬ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 𝑄 )
54 53 neqned ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑄 )
55 54 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑄 )
56 55 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑄 )
57 eqid ⊢ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) )
58 5 7 2 57 11 isirred ⊢ ( 𝑄 ∈ 𝐼 ↔ ( 𝑄 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ≠ 𝑄 ) )
59 9 56 58 sylanbrc ⊢ ( 𝜑 → 𝑄 ∈ 𝐼 )