Metamath Proof Explorer

Theorem 2zrngnring

Description: R is not a unital ring. (Contributed by AV, 6-Jan-2020)

Ref Expression
Hypotheses 2zrng.e ⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2zrngbas.r ⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
2zrngmmgm.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
Assertion 2zrngnring 𝑅 ∉ Ring

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2 2zrngbas.r ⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3 2zrngmmgm.1 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4 1 2 3 2zrngnmlid ⊢ ∀ 𝑏 ∈ 𝐸 ∃ 𝑎 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎
5 1 2 2zrngbas ⊢ 𝐸 = ( Base ‘ 𝑅 )
6 3 5 mgpbas ⊢ 𝐸 = ( Base ‘ 𝑀 )
7 1 2 2zrngmul ⊢ · = ( .r ‘ 𝑅 )
8 3 7 mgpplusg ⊢ · = ( +g ‘ 𝑀 )
9 6 8 isnmnd ⊢ ( ∀ 𝑏 ∈ 𝐸 ∃ 𝑎 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎 → 𝑀 ∉ Mnd )
10 df-nel ⊢ ( 𝑀 ∉ Mnd ↔ ¬ 𝑀 ∈ Mnd )
11 9 10 sylib ⊢ ( ∀ 𝑏 ∈ 𝐸 ∃ 𝑎 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎 → ¬ 𝑀 ∈ Mnd )
12 4 11 ax-mp ⊢ ¬ 𝑀 ∈ Mnd
13 12 3mix2i ⊢ ( ¬ 𝑅 ∈ Grp ∨ ¬ 𝑀 ∈ Mnd ∨ ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) )
14 3ianor ⊢ ( ¬ ( 𝑅 ∈ Grp ∧ 𝑀 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) ) ↔ ( ¬ 𝑅 ∈ Grp ∨ ¬ 𝑀 ∈ Mnd ∨ ¬ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) ) )
15 13 14 mpbir ⊢ ¬ ( 𝑅 ∈ Grp ∧ 𝑀 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) )
16 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
17 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
18 16 3 17 7 isring ⊢ ( 𝑅 ∈ Ring ↔ ( 𝑅 ∈ Grp ∧ 𝑀 ∈ Mnd ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ ( Base ‘ 𝑅 ) ∀ 𝑧 ∈ ( Base ‘ 𝑅 ) ( ( 𝑥 · ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 · 𝑧 ) ) ∧ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 · 𝑧 ) ) ) ) )
19 15 18 mtbir ⊢ ¬ 𝑅 ∈ Ring
20 19 nelir ⊢ 𝑅 ∉ Ring