Metamath Proof Explorer

Theorem 2zrngnmlid

Description: R has no multiplicative (left) identity. (Contributed by AV, 12-Feb-2020)

Ref Expression
Hypotheses 2zrng.e ⊢E=z∈ℤ|∃x∈ℤz=2⁢x
2zrngbas.r ⊢R=ℂfld↾𝑠E
2zrngmmgm.1 ⊢M=mulGrpR
Assertion 2zrngnmlid ⊢∀b∈E∃a∈Eb⁢a≠a

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢E=z∈ℤ|∃x∈ℤz=2⁢x
2 2zrngbas.r ⊢R=ℂfld↾𝑠E
3 2zrngmmgm.1 ⊢M=mulGrpR
4 1 2even ⊢2∈E
5 4 a1i ⊢b∈E→2∈E
6 oveq2 ⊢a=2→b⁢a=b⋅2
7 id ⊢a=2→a=2
8 6 7 neeq12d ⊢a=2→b⁢a≠a↔b⋅2≠2
9 8 adantl ⊢b∈E∧a=2→b⁢a≠a↔b⋅2≠2
10 elrabi ⊢b∈z∈ℤ|∃x∈ℤz=2⁢x→b∈ℤ
11 10 zcnd ⊢b∈z∈ℤ|∃x∈ℤz=2⁢x→b∈ℂ
12 11 1 eleq2s ⊢b∈E→b∈ℂ
13 1 1neven ⊢1∉E
14 elnelne2 ⊢b∈E∧1∉E→b≠1
15 13 14 mpan2 ⊢b∈E→b≠1
16 15 adantr ⊢b∈E∧b∈ℂ→b≠1
17 simpr ⊢b∈E∧b∈ℂ→b∈ℂ
18 2cnd ⊢b∈E∧b∈ℂ→2∈ℂ
19 2ne0 ⊢2≠0
20 19 a1i ⊢b∈E∧b∈ℂ→2≠0
21 17 18 20 divcan4d ⊢b∈E∧b∈ℂ→b⋅22=b
22 2cnne0 ⊢2∈ℂ∧2≠0
23 divid ⊢2∈ℂ∧2≠0→22=1
24 22 23 mp1i ⊢b∈E∧b∈ℂ→22=1
25 16 21 24 3netr4d ⊢b∈E∧b∈ℂ→b⋅22≠22
26 17 18 mulcld ⊢b∈E∧b∈ℂ→b⋅2∈ℂ
27 22 a1i ⊢b∈E∧b∈ℂ→2∈ℂ∧2≠0
28 div11 ⊢b⋅2∈ℂ∧2∈ℂ∧2∈ℂ∧2≠0→b⋅22=22↔b⋅2=2
29 26 18 27 28 syl3anc ⊢b∈E∧b∈ℂ→b⋅22=22↔b⋅2=2
30 29 biimprd ⊢b∈E∧b∈ℂ→b⋅2=2→b⋅22=22
31 30 necon3d ⊢b∈E∧b∈ℂ→b⋅22≠22→b⋅2≠2
32 25 31 mpd ⊢b∈E∧b∈ℂ→b⋅2≠2
33 12 32 mpdan ⊢b∈E→b⋅2≠2
34 5 9 33 rspcedvd ⊢b∈E→∃a∈Eb⁢a≠a
35 34 rgen ⊢∀b∈E∃a∈Eb⁢a≠a