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 ∧ 𝑋𝐼𝑌𝑈 ) → ( 𝑋 · 𝑌 ) ∈ 𝐼 )