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 ∧ 𝑋𝐼 ) → ( 𝑋 = 00𝐼 ) )
29 28 necon3bd ( ( 𝑅 ∈ Ring ∧ 𝑋𝐼 ) → ( ¬ 0𝐼𝑋0 ) )
30 25 29 mpd ( ( 𝑅 ∈ Ring ∧ 𝑋𝐼 ) → 𝑋0 )