Metamath Proof Explorer

Theorem mxidlirredi

Description: In an integral domain, the generator of a maximal ideal is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses mxidlirredi.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mxidlirredi.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
mxidlirredi.0 ⊢ 0 = ( 0g ‘ 𝑅 )
mxidlirredi.m ⊢ 𝑀 = ( 𝐾 ‘ { 𝑋 } )
mxidlirredi.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
mxidlirredi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mxidlirredi.y ⊢ ( 𝜑 → 𝑋 ≠ 0 )
mxidlirredi.1 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
Assertion mxidlirredi ( 𝜑 → 𝑋 ∈ ( Irred ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 mxidlirredi.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mxidlirredi.k ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3 mxidlirredi.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 mxidlirredi.m ⊢ 𝑀 = ( 𝐾 ‘ { 𝑋 } )
5 mxidlirredi.r ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
6 mxidlirredi.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 mxidlirredi.y ⊢ ( 𝜑 → 𝑋 ≠ 0 )
8 mxidlirredi.1 ⊢ ( 𝜑 → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
9 5 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 1 mxidlnr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) ) → 𝑀 ≠ 𝐵 )
11 9 8 10 syl2anc ⊢ ( 𝜑 → 𝑀 ≠ 𝐵 )
12 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
13 5 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
14 12 2 4 1 6 13 unitpidl1 ⊢ ( 𝜑 → ( 𝑀 = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
15 14 necon3abid ⊢ ( 𝜑 → ( 𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
16 11 15 mpbid ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
17 6 16 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
18 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑅 ∈ Ring )
19 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
20 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
21 20 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ 𝐵 )
22 21 snssd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → { 𝑔 } ⊆ 𝐵 )
23 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
24 2 1 23 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑔 } ⊆ 𝐵 ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝑅 ) )
25 18 22 24 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝑅 ) )
26 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ Ring )
27 26 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ Ring )
28 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
29 28 eldifad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ 𝐵 )
30 oveq1 ⊢ ( 𝑦 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) )
31 30 eqeq2d ⊢ ( 𝑦 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) → ( 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ↔ 𝑥 = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) ) )
32 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑞 ∈ 𝐵 )
34 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
35 34 eldifad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ 𝐵 )
36 1 32 27 33 35 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝐵 )
37 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
38 37 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) )
39 1 32 27 33 35 29 ringassd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) = ( 𝑞 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) )
40 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) )
41 38 39 40 3eqtr4rd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑥 = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) )
42 31 36 41 rspcedvdw ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) )
43 1 32 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ) )
44 43 biimpar ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ) → 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) )
45 27 29 42 44 syl21anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) )
46 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → 𝑋 ∈ 𝐵 )
47 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → 𝑥 ∈ 𝑀 )
48 47 4 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) )
49 1 32 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑞 ∈ 𝐵 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) )
50 49 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ∃ 𝑞 ∈ 𝐵 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) )
51 26 46 48 50 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → ∃ 𝑞 ∈ 𝐵 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) )
52 45 51 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) )
53 52 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( 𝑥 ∈ 𝑀 → 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) ) )
54 53 ssrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑀 ⊆ ( 𝐾 ‘ { 𝑔 } ) )
55 2 1 rspssid ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑔 } ⊆ 𝐵 ) → { 𝑔 } ⊆ ( 𝐾 ‘ { 𝑔 } ) )
56 vex ⊢ 𝑔 ∈ V
57 56 snss ⊢ ( 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) ↔ { 𝑔 } ⊆ ( 𝐾 ‘ { 𝑔 } ) )
58 55 57 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑔 } ⊆ 𝐵 ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) )
59 18 22 58 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) )
60 13 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ CRing )
61 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑟 ∈ 𝐵 )
62 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
63 62 eldifad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ 𝐵 )
64 18 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑅 ∈ Ring )
65 64 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ Ring )
66 1 32 65 61 63 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝐵 )
67 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
68 1 67 9 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
69 68 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
70 21 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ 𝐵 )
71 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑔 = 0 )
72 71 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = ( 𝑓 ( .r ‘ 𝑅 ) 0 ) )
73 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
74 64 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑅 ∈ Ring )
75 63 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑓 ∈ 𝐵 )
76 1 32 3 74 75 ringrzd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ( 𝑓 ( .r ‘ 𝑅 ) 0 ) = 0 )
77 72 73 76 3eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑋 = 0 )
78 7 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = 0 )
79 78 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ¬ 𝑋 = 0 )
80 77 79 pm2.65da ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ¬ 𝑔 = 0 )
81 80 neqned ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ≠ 0 )
82 70 81 eldifsnd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ ( 𝐵 ∖ { 0 } ) )
83 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ IDomn )
84 1 32 67 65 70 ringlidmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑔 ) = 𝑔 )
85 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
86 1 32 65 61 63 70 ringassd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) = ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) )
87 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
88 87 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
89 86 88 eqtr2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) )
90 84 85 89 3eqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑔 ) )
91 1 3 32 66 69 82 83 90 idomrcan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) = ( 1r ‘ 𝑅 ) )
92 12 67 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
93 9 92 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
94 93 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
95 91 94 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Unit ‘ 𝑅 ) )
96 12 32 1 unitmulclb ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑟 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑟 ∈ ( Unit ‘ 𝑅 ) ∧ 𝑓 ∈ ( Unit ‘ 𝑅 ) ) ) )
97 96 simplbda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑟 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑓 ∈ ( Unit ‘ 𝑅 ) )
98 60 61 63 95 97 syl31anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ ( Unit ‘ 𝑅 ) )
99 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑋 ∈ 𝐵 )
100 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑔 ∈ 𝑀 )
101 100 4 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑋 } ) )
102 1 32 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑟 ∈ 𝐵 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) )
103 102 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ∃ 𝑟 ∈ 𝐵 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
104 64 99 101 103 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → ∃ 𝑟 ∈ 𝐵 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
105 98 104 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑓 ∈ ( Unit ‘ 𝑅 ) )
106 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
107 106 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → ¬ 𝑓 ∈ ( Unit ‘ 𝑅 ) )
108 105 107 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ¬ 𝑔 ∈ 𝑀 )
109 59 108 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( ( 𝐾 ‘ { 𝑔 } ) ∖ 𝑀 ) )
110 1 18 19 25 54 109 mxidlmaxv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( 𝐾 ‘ { 𝑔 } ) = 𝐵 )
111 eqid ⊢ ( 𝐾 ‘ { 𝑔 } ) = ( 𝐾 ‘ { 𝑔 } )
112 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑅 ∈ CRing )
113 12 2 111 1 21 112 unitpidl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( ( 𝐾 ‘ { 𝑔 } ) = 𝐵 ↔ 𝑔 ∈ ( Unit ‘ 𝑅 ) ) )
114 110 113 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( Unit ‘ 𝑅 ) )
115 20 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ¬ 𝑔 ∈ ( Unit ‘ 𝑅 ) )
116 114 115 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) → ¬ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
117 116 anasss ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ) → ¬ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
118 117 neqned ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ≠ 𝑋 )
119 118 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ≠ 𝑋 )
120 eqid ⊢ ( Irred ‘ 𝑅 ) = ( Irred ‘ 𝑅 )
121 eqid ⊢ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) = ( 𝐵 ∖ ( Unit ‘ 𝑅 ) )
122 1 12 120 121 32 isirred ⊢ ( 𝑋 ∈ ( Irred ‘ 𝑅 ) ↔ ( 𝑋 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ≠ 𝑋 ) )
123 17 119 122 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( Irred ‘ 𝑅 ) )