Metamath Proof Explorer

Theorem isnirred

Description: The property of being a non-irreducible (reducible) element in a ring. (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 isnirred ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ) )

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 4 eleq2i ⊢ ( 𝑋 ∈ 𝑁 ↔ 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) )
7 eldif ⊢ ( 𝑋 ∈ ( 𝐵 ∖ 𝑈 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) )
8 6 7 bitri ⊢ ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝑈 ) )
9 8 baibr ⊢ ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ 𝑁 ) )
10 df-ne ⊢ ( ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ¬ ( 𝑥 · 𝑦 ) = 𝑋 )
11 10 ralbii ⊢ ( ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ∀ 𝑦 ∈ 𝑁 ¬ ( 𝑥 · 𝑦 ) = 𝑋 )
12 ralnex ⊢ ( ∀ 𝑦 ∈ 𝑁 ¬ ( 𝑥 · 𝑦 ) = 𝑋 ↔ ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
13 11 12 bitri ⊢ ( ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
14 13 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ↔ ∀ 𝑥 ∈ 𝑁 ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
15 ralnex ⊢ ( ∀ 𝑥 ∈ 𝑁 ¬ ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ↔ ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 )
16 14 15 bitr2i ⊢ ( ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 )
17 16 a1i ⊢ ( 𝑋 ∈ 𝐵 → ( ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ↔ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
18 9 17 anbi12d ⊢ ( 𝑋 ∈ 𝐵 → ( ( ¬ 𝑋 ∈ 𝑈 ∧ ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) ) )
19 ioran ⊢ ( ¬ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ↔ ( ¬ 𝑋 ∈ 𝑈 ∧ ¬ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) )
20 1 2 3 4 5 isirred ⊢ ( 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑁 ∧ ∀ 𝑥 ∈ 𝑁 ∀ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) ≠ 𝑋 ) )
21 18 19 20 3bitr4g ⊢ ( 𝑋 ∈ 𝐵 → ( ¬ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ↔ 𝑋 ∈ 𝐼 ) )
22 21 con1bid ⊢ ( 𝑋 ∈ 𝐵 → ( ¬ 𝑋 ∈ 𝐼 ↔ ( 𝑋 ∈ 𝑈 ∨ ∃ 𝑥 ∈ 𝑁 ∃ 𝑦 ∈ 𝑁 ( 𝑥 · 𝑦 ) = 𝑋 ) ) )