Metamath Proof Explorer

Theorem irredn0

Description: The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014)

Ref Expression
Hypotheses irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
irredn0.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion irredn0 ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ≠ 0 )

Proof

Step Hyp Ref Expression
1 irredn0.i ⊢ 𝐼 = ( Irred ‘ 𝑅 )
2 irredn0.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 3 2 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
5 4 anim1i ⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 0 ∈ ( Unit ‘ 𝑅 ) ) → ( 0 ∈ ( Base ‘ 𝑅 ) ∧ ¬ 0 ∈ ( Unit ‘ 𝑅 ) ) )
6 eldif ⊢ ( 0 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ↔ ( 0 ∈ ( Base ‘ 𝑅 ) ∧ ¬ 0 ∈ ( Unit ‘ 𝑅 ) ) )
7 5 6 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 0 ∈ ( Unit ‘ 𝑅 ) ) → 0 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) )
8 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
9 3 8 2 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ ( Base ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 )
10 4 9 mpdan ⊢ ( 𝑅 ∈ Ring → ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 )
11 10 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 0 ∈ ( Unit ‘ 𝑅 ) ) → ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 )
12 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0 ( .r ‘ 𝑅 ) 𝑦 ) )
13 12 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ↔ ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) )
14 oveq2 ⊢ ( 𝑦 = 0 → ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = ( 0 ( .r ‘ 𝑅 ) 0 ) )
15 14 eqeq1d ⊢ ( 𝑦 = 0 → ( ( 0 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ↔ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) )
16 13 15 rspc2ev ⊢ ( ( 0 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ 0 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∧ ( 0 ( .r ‘ 𝑅 ) 0 ) = 0 ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 )
17 7 7 11 16 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ ¬ 0 ∈ ( Unit ‘ 𝑅 ) ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 )
18 17 ex ⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ ( Unit ‘ 𝑅 ) → ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) )
19 18 orrd ⊢ ( 𝑅 ∈ Ring → ( 0 ∈ ( Unit ‘ 𝑅 ) ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) )
20 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
21 eqid ⊢ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) )
22 3 20 1 21 8 isnirred ⊢ ( 0 ∈ ( Base ‘ 𝑅 ) → ( ¬ 0 ∈ 𝐼 ↔ ( 0 ∈ ( Unit ‘ 𝑅 ) ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) ) )
23 4 22 syl ⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ 𝐼 ↔ ( 0 ∈ ( Unit ‘ 𝑅 ) ∨ ∃ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ∃ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ∖ ( Unit ‘ 𝑅 ) ) ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = 0 ) ) )
24 19 23 mpbird ⊢ ( 𝑅 ∈ Ring → ¬ 0 ∈ 𝐼 )
25 24 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ¬ 0 ∈ 𝐼 )
26 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ∈ 𝐼 )
27 eleq1 ⊢ ( 𝑋 = 0 → ( 𝑋 ∈ 𝐼 ↔ 0 ∈ 𝐼 ) )
28 26 27 syl5ibcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( 𝑋 = 0 → 0 ∈ 𝐼 ) )
29 28 necon3bd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → ( ¬ 0 ∈ 𝐼 → 𝑋 ≠ 0 ) )
30 25 29 mpd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐼 ) → 𝑋 ≠ 0 )