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 12 2 4 1 6 5 unitpidl1 ⊢ ( 𝜑 → ( 𝑀 = 𝐵 ↔ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
14 13 necon3abid ⊢ ( 𝜑 → ( 𝑀 ≠ 𝐵 ↔ ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) ) )
15 11 14 mpbid ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( Unit ‘ 𝑅 ) )
16 6 15 eldifd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
17 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑅 ∈ Ring )
18 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑀 ∈ ( MaxIdeal ‘ 𝑅 ) )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
20 19 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ 𝐵 )
21 20 snssd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → { 𝑔 } ⊆ 𝐵 )
22 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
23 2 1 22 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑔 } ⊆ 𝐵 ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝑅 ) )
24 17 21 23 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( 𝐾 ‘ { 𝑔 } ) ∈ ( LIdeal ‘ 𝑅 ) )
25 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) → 𝑅 ∈ Ring )
26 25 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ Ring )
27 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
28 27 eldifad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ 𝐵 )
29 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
30 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑞 ∈ 𝐵 )
31 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
32 31 eldifad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ 𝐵 )
33 1 29 26 30 32 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝐵 )
34 oveq1 ⊢ ( 𝑦 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) )
35 34 eqeq2d ⊢ ( 𝑦 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) → ( 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ↔ 𝑥 = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) ) )
36 35 adantl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑦 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ) → ( 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ↔ 𝑥 = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) ) )
37 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
38 37 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) )
39 1 29 26 30 32 28 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 33 36 41 rspcedvd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑥 ∈ 𝑀 ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) )
43 1 29 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ) )
44 43 biimpar ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑔 ∈ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐵 𝑥 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑔 ) ) → 𝑥 ∈ ( 𝐾 ‘ { 𝑔 } ) )
45 26 28 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 29 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑞 ∈ 𝐵 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) ) )
50 49 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ∃ 𝑞 ∈ 𝐵 𝑥 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑋 ) )
51 25 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 17 21 58 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑔 } ) )
60 df-idom ⊢ IDomn = ( CRing ∩ Domn )
61 5 60 eleqtrdi ⊢ ( 𝜑 → 𝑅 ∈ ( CRing ∩ Domn ) )
62 61 elin1d ⊢ ( 𝜑 → 𝑅 ∈ CRing )
63 62 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ CRing )
64 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑟 ∈ 𝐵 )
65 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
66 65 eldifad ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ 𝐵 )
67 17 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑅 ∈ Ring )
68 67 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ Ring )
69 1 29 68 64 66 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝐵 )
70 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
71 1 70 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
72 9 71 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
73 72 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
74 20 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ 𝐵 )
75 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑔 = 0 )
76 75 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = ( 𝑓 ( .r ‘ 𝑅 ) 0 ) )
77 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
78 67 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑅 ∈ Ring )
79 66 adantr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑓 ∈ 𝐵 )
80 1 29 3 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑓 ∈ 𝐵 ) → ( 𝑓 ( .r ‘ 𝑅 ) 0 ) = 0 )
81 78 79 80 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ( 𝑓 ( .r ‘ 𝑅 ) 0 ) = 0 )
82 76 77 81 3eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → 𝑋 = 0 )
83 7 neneqd ⊢ ( 𝜑 → ¬ 𝑋 = 0 )
84 83 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) ∧ 𝑔 = 0 ) → ¬ 𝑋 = 0 )
85 82 84 pm2.65da ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ¬ 𝑔 = 0 )
86 85 neqned ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ≠ 0 )
87 eldifsn ⊢ ( 𝑔 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑔 ∈ 𝐵 ∧ 𝑔 ≠ 0 ) )
88 74 86 87 sylanbrc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 ∈ ( 𝐵 ∖ { 0 } ) )
89 5 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ IDomn )
90 1 29 70 68 74 ringlidmd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑔 ) = 𝑔 )
91 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
92 1 29 68 64 66 74 ringassd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) = ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) )
93 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
94 93 oveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ) = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
95 92 94 eqtr2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) = ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) )
96 90 91 95 3eqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ( .r ‘ 𝑅 ) 𝑔 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑔 ) )
97 1 3 29 69 73 88 89 96 idomrcan ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) = ( 1r ‘ 𝑅 ) )
98 12 70 1unit ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
99 9 98 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
100 99 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
101 97 100 eqeltrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Unit ‘ 𝑅 ) )
102 12 29 1 unitmulclb ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑟 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) → ( ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( 𝑟 ∈ ( Unit ‘ 𝑅 ) ∧ 𝑓 ∈ ( Unit ‘ 𝑅 ) ) ) )
103 102 simplbda ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑟 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ∧ ( 𝑟 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( Unit ‘ 𝑅 ) ) → 𝑓 ∈ ( Unit ‘ 𝑅 ) )
104 63 64 66 101 103 syl31anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) ∧ 𝑟 ∈ 𝐵 ) ∧ 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑓 ∈ ( Unit ‘ 𝑅 ) )
105 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑋 ∈ 𝐵 )
106 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑔 ∈ 𝑀 )
107 106 4 eleqtrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑔 ∈ ( 𝐾 ‘ { 𝑋 } ) )
108 1 29 2 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑔 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ ∃ 𝑟 ∈ 𝐵 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) ) )
109 108 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑔 ∈ ( 𝐾 ‘ { 𝑋 } ) ) → ∃ 𝑟 ∈ 𝐵 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
110 67 105 107 109 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → ∃ 𝑟 ∈ 𝐵 𝑔 = ( 𝑟 ( .r ‘ 𝑅 ) 𝑋 ) )
111 104 110 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑓 ∈ ( Unit ‘ 𝑅 ) )
112 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) )
113 112 eldifbd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) ∧ 𝑔 ∈ 𝑀 ) → ¬ 𝑓 ∈ ( Unit ‘ 𝑅 ) )
114 111 113 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ¬ 𝑔 ∈ 𝑀 )
115 59 114 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( ( 𝐾 ‘ { 𝑔 } ) ∖ 𝑀 ) )
116 1 17 18 24 54 115 mxidlmaxv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( 𝐾 ‘ { 𝑔 } ) = 𝐵 )
117 eqid ⊢ ( 𝐾 ‘ { 𝑔 } ) = ( 𝐾 ‘ { 𝑔 } )
118 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑅 ∈ IDomn )
119 12 2 117 1 20 118 unitpidl1 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ( ( 𝐾 ‘ { 𝑔 } ) = 𝐵 ↔ 𝑔 ∈ ( Unit ‘ 𝑅 ) ) )
120 116 119 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → 𝑔 ∈ ( Unit ‘ 𝑅 ) )
121 19 eldifbd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 ) → ¬ 𝑔 ∈ ( Unit ‘ 𝑅 ) )
122 120 121 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) → ¬ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
123 122 anasss ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ) → ¬ ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) = 𝑋 )
124 123 neqned ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∧ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ) ) → ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ≠ 𝑋 )
125 124 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ≠ 𝑋 )
126 eqid ⊢ ( Irred ‘ 𝑅 ) = ( Irred ‘ 𝑅 )
127 eqid ⊢ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) = ( 𝐵 ∖ ( Unit ‘ 𝑅 ) )
128 1 12 126 127 29 isirred ⊢ ( 𝑋 ∈ ( Irred ‘ 𝑅 ) ↔ ( 𝑋 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∧ ∀ 𝑓 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ∀ 𝑔 ∈ ( 𝐵 ∖ ( Unit ‘ 𝑅 ) ) ( 𝑓 ( .r ‘ 𝑅 ) 𝑔 ) ≠ 𝑋 ) )
129 16 125 128 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ ( Irred ‘ 𝑅 ) )