Metamath Proof Explorer

Theorem 2zrngnmrid

Description: R has no multiplicative (right) 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 = mulGrp R
Assertion 2zrngnmrid ⊢ ∀ a ∈ E ∖ 0 ∀ b ∈ E a ⁢ b ≠ 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 = mulGrp R
4 eldifsn ⊢ a ∈ E ∖ 0 ↔ a ∈ E ∧ a ≠ 0
5 eqeq1 ⊢ z = a → z = 2 ⁢ x ↔ a = 2 ⁢ x
6 5 rexbidv ⊢ z = a → ∃ x ∈ ℤ z = 2 ⁢ x ↔ ∃ x ∈ ℤ a = 2 ⁢ x
7 6 1 elrab2 ⊢ a ∈ E ↔ a ∈ ℤ ∧ ∃ x ∈ ℤ a = 2 ⁢ x
8 zcn ⊢ a ∈ ℤ → a ∈ ℂ
9 8 adantr ⊢ a ∈ ℤ ∧ ∃ x ∈ ℤ a = 2 ⁢ x → a ∈ ℂ
10 7 9 sylbi ⊢ a ∈ E → a ∈ ℂ
11 10 anim1i ⊢ a ∈ E ∧ a ≠ 0 → a ∈ ℂ ∧ a ≠ 0
12 4 11 sylbi ⊢ a ∈ E ∖ 0 → a ∈ ℂ ∧ a ≠ 0
13 eqeq1 ⊢ z = b → z = 2 ⁢ x ↔ b = 2 ⁢ x
14 13 rexbidv ⊢ z = b → ∃ x ∈ ℤ z = 2 ⁢ x ↔ ∃ x ∈ ℤ b = 2 ⁢ x
15 14 1 elrab2 ⊢ b ∈ E ↔ b ∈ ℤ ∧ ∃ x ∈ ℤ b = 2 ⁢ x
16 zcn ⊢ b ∈ ℤ → b ∈ ℂ
17 16 adantr ⊢ b ∈ ℤ ∧ ∃ x ∈ ℤ b = 2 ⁢ x → b ∈ ℂ
18 15 17 sylbi ⊢ b ∈ E → b ∈ ℂ
19 18 ancli ⊢ b ∈ E → b ∈ E ∧ b ∈ ℂ
20 1 1neven ⊢ 1 ∉ E
21 elnelne2 ⊢ b ∈ E ∧ 1 ∉ E → b ≠ 1
22 20 21 mpan2 ⊢ b ∈ E → b ≠ 1
23 22 ad2antrl ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → b ≠ 1
24 simpr ⊢ b ∈ E ∧ b ∈ ℂ → b ∈ ℂ
25 24 anim2i ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ ℂ
26 3anass ⊢ b ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0 ↔ b ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0
27 ancom ⊢ b ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0 ↔ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ ℂ
28 26 27 bitri ⊢ b ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0 ↔ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ ℂ
29 25 28 sylibr ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → b ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0
30 divcan3 ⊢ b ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0 → a ⁢ b a = b
31 29 30 syl ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b a = b
32 divid ⊢ a ∈ ℂ ∧ a ≠ 0 → a a = 1
33 32 adantr ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a a = 1
34 23 31 33 3netr4d ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b a ≠ a a
35 simpl ⊢ a ∈ ℂ ∧ a ≠ 0 → a ∈ ℂ
36 mulcl ⊢ a ∈ ℂ ∧ b ∈ ℂ → a ⁢ b ∈ ℂ
37 35 24 36 syl2an ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b ∈ ℂ
38 35 adantr ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ∈ ℂ
39 simpl ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ∈ ℂ ∧ a ≠ 0
40 div11 ⊢ a ⁢ b ∈ ℂ ∧ a ∈ ℂ ∧ a ∈ ℂ ∧ a ≠ 0 → a ⁢ b a = a a ↔ a ⁢ b = a
41 37 38 39 40 syl3anc ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b a = a a ↔ a ⁢ b = a
42 41 biimprd ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b = a → a ⁢ b a = a a
43 42 necon3d ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b a ≠ a a → a ⁢ b ≠ a
44 34 43 mpd ⊢ a ∈ ℂ ∧ a ≠ 0 ∧ b ∈ E ∧ b ∈ ℂ → a ⁢ b ≠ a
45 12 19 44 syl2an ⊢ a ∈ E ∖ 0 ∧ b ∈ E → a ⁢ b ≠ a
46 45 rgen2 ⊢ ∀ a ∈ E ∖ 0 ∀ b ∈ E a ⁢ b ≠ a