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

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 ⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )