Metamath Proof Explorer


Theorem isirred

Description: An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irred.1 𝐵 = ( Base ‘ 𝑅 )
irred.2 𝑈 = ( Unit ‘ 𝑅 )
irred.3 𝐼 = ( Irred ‘ 𝑅 )
irred.4 𝑁 = ( 𝐵𝑈 )
irred.5 · = ( .r𝑅 )
Assertion isirred ( 𝑋𝐼 ↔ ( 𝑋𝑁 ∧ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 irred.1 𝐵 = ( Base ‘ 𝑅 )
2 irred.2 𝑈 = ( Unit ‘ 𝑅 )
3 irred.3 𝐼 = ( Irred ‘ 𝑅 )
4 irred.4 𝑁 = ( 𝐵𝑈 )
5 irred.5 · = ( .r𝑅 )
6 elfvdm ( 𝑋 ∈ ( Irred ‘ 𝑅 ) → 𝑅 ∈ dom Irred )
7 6 3 eleq2s ( 𝑋𝐼𝑅 ∈ dom Irred )
8 7 elexd ( 𝑋𝐼𝑅 ∈ V )
9 eldifi ( 𝑋 ∈ ( 𝐵𝑈 ) → 𝑋𝐵 )
10 9 4 eleq2s ( 𝑋𝑁𝑋𝐵 )
11 10 1 eleqtrdi ( 𝑋𝑁𝑋 ∈ ( Base ‘ 𝑅 ) )
12 11 elfvexd ( 𝑋𝑁𝑅 ∈ V )
13 12 adantr ( ( 𝑋𝑁 ∧ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) → 𝑅 ∈ V )
14 fvex ( Base ‘ 𝑟 ) ∈ V
15 difexg ( ( Base ‘ 𝑟 ) ∈ V → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ∈ V )
16 14 15 mp1i ( 𝑟 = 𝑅 → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ∈ V )
17 simpr ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) )
18 simpl ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑟 = 𝑅 )
19 18 fveq2d ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
20 19 1 eqtr4di ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Base ‘ 𝑟 ) = 𝐵 )
21 18 fveq2d ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Unit ‘ 𝑟 ) = ( Unit ‘ 𝑅 ) )
22 21 2 eqtr4di ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( Unit ‘ 𝑟 ) = 𝑈 )
23 20 22 difeq12d ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) = ( 𝐵𝑈 ) )
24 23 4 eqtr4di ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) = 𝑁 )
25 17 24 eqtrd ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → 𝑏 = 𝑁 )
26 18 fveq2d ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( .r𝑟 ) = ( .r𝑅 ) )
27 26 5 eqtr4di ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( .r𝑟 ) = · )
28 27 oveqd ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( 𝑥 ( .r𝑟 ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
29 28 neeq1d ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ( 𝑥 ( .r𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ( 𝑥 · 𝑦 ) ≠ 𝑧 ) )
30 25 29 raleqbidv ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ∀ 𝑦𝑏 ( 𝑥 ( .r𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ) )
31 25 30 raleqbidv ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 ( .r𝑟 ) 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ) )
32 25 31 rabeqbidv ( ( 𝑟 = 𝑅𝑏 = ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) ) → { 𝑧𝑏 ∣ ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 ( .r𝑟 ) 𝑦 ) ≠ 𝑧 } = { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
33 16 32 csbied ( 𝑟 = 𝑅 ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) / 𝑏 { 𝑧𝑏 ∣ ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 ( .r𝑟 ) 𝑦 ) ≠ 𝑧 } = { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
34 df-irred Irred = ( 𝑟 ∈ V ↦ ( ( Base ‘ 𝑟 ) ∖ ( Unit ‘ 𝑟 ) ) / 𝑏 { 𝑧𝑏 ∣ ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 ( .r𝑟 ) 𝑦 ) ≠ 𝑧 } )
35 fvex ( Base ‘ 𝑅 ) ∈ V
36 1 35 eqeltri 𝐵 ∈ V
37 36 difexi ( 𝐵𝑈 ) ∈ V
38 4 37 eqeltri 𝑁 ∈ V
39 38 rabex { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ∈ V
40 33 34 39 fvmpt ( 𝑅 ∈ V → ( Irred ‘ 𝑅 ) = { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
41 3 40 eqtrid ( 𝑅 ∈ V → 𝐼 = { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } )
42 41 eleq2d ( 𝑅 ∈ V → ( 𝑋𝐼𝑋 ∈ { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ) )
43 neeq2 ( 𝑧 = 𝑋 → ( ( 𝑥 · 𝑦 ) ≠ 𝑧 ↔ ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
44 43 2ralbidv ( 𝑧 = 𝑋 → ( ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 ↔ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
45 44 elrab ( 𝑋 ∈ { 𝑧𝑁 ∣ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑧 } ↔ ( 𝑋𝑁 ∧ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
46 42 45 bitrdi ( 𝑅 ∈ V → ( 𝑋𝐼 ↔ ( 𝑋𝑁 ∧ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) )
47 8 13 46 pm5.21nii ( 𝑋𝐼 ↔ ( 𝑋𝑁 ∧ ∀ 𝑥𝑁𝑦𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )