Metamath Proof Explorer

Theorem 2zrngnmlid2

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 = mulGrp R
Assertion 2zrngnmlid2 ⊢ ∀ a ∈ E ∖ 0 ∀ b ∈ E b ⁢ 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 = mulGrp R
4 1 2 3 2zrngnmrid ⊢ ∀ a ∈ E ∖ 0 ∀ b ∈ E a ⁢ b ≠ a
5 eldifi ⊢ a ∈ E ∖ 0 → a ∈ E
6 elrabi ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℤ
7 6 zcnd ⊢ a ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → a ∈ ℂ
8 7 1 eleq2s ⊢ a ∈ E → a ∈ ℂ
9 5 8 syl ⊢ a ∈ E ∖ 0 → a ∈ ℂ
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 mulcom ⊢ a ∈ ℂ ∧ b ∈ ℂ → a ⁢ b = b ⁢ a
14 9 12 13 syl2an ⊢ a ∈ E ∖ 0 ∧ b ∈ E → a ⁢ b = b ⁢ a
15 14 eqcomd ⊢ a ∈ E ∖ 0 ∧ b ∈ E → b ⁢ a = a ⁢ b
16 15 eqeq1d ⊢ a ∈ E ∖ 0 ∧ b ∈ E → b ⁢ a = a ↔ a ⁢ b = a
17 16 biimpd ⊢ a ∈ E ∖ 0 ∧ b ∈ E → b ⁢ a = a → a ⁢ b = a
18 17 necon3d ⊢ a ∈ E ∖ 0 ∧ b ∈ E → a ⁢ b ≠ a → b ⁢ a ≠ a
19 18 ralimdva ⊢ a ∈ E ∖ 0 → ∀ b ∈ E a ⁢ b ≠ a → ∀ b ∈ E b ⁢ a ≠ a
20 19 ralimia ⊢ ∀ a ∈ E ∖ 0 ∀ b ∈ E a ⁢ b ≠ a → ∀ a ∈ E ∖ 0 ∀ b ∈ E b ⁢ a ≠ a
21 4 20 ax-mp ⊢ ∀ a ∈ E ∖ 0 ∀ b ∈ E b ⁢ a ≠ a