This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem irredrmul

Description: The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
irredrmul.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
irredrmul.t ⊢ · = ( .r ‘ 𝑅 )
Assertion irredrmul ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
2 irredrmul.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
3 irredrmul.t ⊢ · = ( .r ‘ 𝑅 )
4 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ 𝐼 )
5 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → 𝑅 ∈ Ring )
6 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ 𝑈 )
7 eqid ⊢ ( /r ‘ 𝑅 ) = ( /r ‘ 𝑅 )
8 2 7 unitdvcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 )
9 8 3com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ ( 𝑋 · 𝑌 ) ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 )
10 9 3expia ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 ) )
11 5 6 10 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 ) )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 1 12 irredcl ⊢ ( 𝑋 ∈ 𝐼 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
14 13 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
15 12 2 7 3 dvrcan3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) = 𝑋 )
16 5 14 6 15 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) = 𝑋 )
17 16 eleq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 ↔ 𝑋 ∈ 𝑈 ) )
18 11 17 sylibd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑋 · 𝑌 ) ∈ 𝑈 → 𝑋 ∈ 𝑈 ) )
19 5 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → 𝑅 ∈ Ring )
20 eldifi ⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
21 20 ad2antrl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
22 6 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → 𝑌 ∈ 𝑈 )
23 12 2 7 dvrcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ 𝑈 ) → ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ ( Base ‘ 𝑅 ) )
24 19 21 22 23 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ ( Base ‘ 𝑅 ) )
25 eldifn ⊢ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) → ¬ 𝑦 ∈ 𝑈 )
26 25 ad2antrl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ¬ 𝑦 ∈ 𝑈 )
27 2 3 unitmulcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) ∈ 𝑈 )
28 27 3com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ∧ ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) ∈ 𝑈 )
29 28 3expia ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) ∈ 𝑈 ) )
30 19 22 29 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) ∈ 𝑈 ) )
31 12 2 7 3 dvrcan1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ 𝑈 ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) = 𝑦 )
32 19 21 22 31 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) = 𝑦 )
33 32 eleq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) · 𝑌 ) ∈ 𝑈 ↔ 𝑦 ∈ 𝑈 ) )
34 30 33 sylibd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 → 𝑦 ∈ 𝑈 ) )
35 26 34 mtod ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ¬ ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ 𝑈 )
36 24 35 eldifd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) )
37 simprr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) )
38 37 oveq1d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( 𝑥 · 𝑦 ) ( /r ‘ 𝑅 ) 𝑌 ) = ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) )
39 eldifi ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
40 39 ad2antlr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
41 12 2 7 3 dvrass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑥 · 𝑦 ) ( /r ‘ 𝑅 ) 𝑌 ) = ( 𝑥 · ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ) )
42 19 40 21 22 41 syl13anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( 𝑥 · 𝑦 ) ( /r ‘ 𝑅 ) 𝑌 ) = ( 𝑥 · ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ) )
43 16 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( ( 𝑋 · 𝑌 ) ( /r ‘ 𝑅 ) 𝑌 ) = 𝑋 )
44 38 42 43 3eqtr3d ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ( 𝑥 · ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ) = 𝑋 )
45 oveq2 ⊢ ( 𝑧 = ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) → ( 𝑥 · 𝑧 ) = ( 𝑥 · ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ) )
46 45 eqeq1d ⊢ ( 𝑧 = ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) → ( ( 𝑥 · 𝑧 ) = 𝑋 ↔ ( 𝑥 · ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ) = 𝑋 ) )
47 46 rspcev ⊢ ( ( ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · ( 𝑦 ( /r ‘ 𝑅 ) 𝑌 ) ) = 𝑋 ) → ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 )
48 36 44 47 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) ∧ ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∧ ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) → ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 )
49 48 rexlimdvaa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ) → ( ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 ) )
50 49 reximdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 ) )
51 18 50 orim12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ( ( 𝑋 · 𝑌 ) ∈ 𝑈 ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) → ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 ) ) )
52 12 2 unitcl ⊢ ( 𝑌 ∈ 𝑈 → 𝑌 ∈ ( Base ‘ 𝑅 ) )
53 52 3ad2ant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ ( Base ‘ 𝑅 ) )
54 12 3 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ 𝑌 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑅 ) )
55 5 14 53 54 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑅 ) )
56 eqid ⊢ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) = ( ( Base ‘ 𝑅 ) ∖ 𝑈 )
57 12 2 1 56 3 isnirred ⊢ ( ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑅 ) → ( ¬ ( 𝑋 · 𝑌 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑌 ) ∈ 𝑈 ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) )
58 55 57 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ¬ ( 𝑋 · 𝑌 ) ∈ 𝐼 ↔ ( ( 𝑋 · 𝑌 ) ∈ 𝑈 ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑦 ) = ( 𝑋 · 𝑌 ) ) ) )
59 12 2 1 56 3 isnirred ⊢ ( 𝑋 ∈ ( Base ‘ 𝑅 ) → ( ¬ 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 ) ) )
60 14 59 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ¬ 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ∃ 𝑧 ∈ ( ( Base ‘ 𝑅 ) ∖ 𝑈 ) ( 𝑥 · 𝑧 ) = 𝑋 ) ) )
61 51 58 60 3imtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( ¬ ( 𝑋 · 𝑌 ) ∈ 𝐼 → ¬ 𝑋 ∈ 𝐼 ) )
62 4 61 mt4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )