Theorem 2zrngnmlid

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

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

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4	1	2even	⊢ 2 ∈ 𝐸
5	4	a1i	⊢ ( 𝑏 ∈ 𝐸 → 2 ∈ 𝐸 )
6		oveq2	⊢ ( 𝑎 = 2 → ( 𝑏 · 𝑎 ) = ( 𝑏 · 2 ) )
7		id	⊢ ( 𝑎 = 2 → 𝑎 = 2 )
8	6 7	neeq12d	⊢ ( 𝑎 = 2 → ( ( 𝑏 · 𝑎 ) ≠ 𝑎 ↔ ( 𝑏 · 2 ) ≠ 2 ) )
9	8	adantl	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑎 = 2 ) → ( ( 𝑏 · 𝑎 ) ≠ 𝑎 ↔ ( 𝑏 · 2 ) ≠ 2 ) )
10		elrabi	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℤ )
11	10	zcnd	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℂ )
12	11 1	eleq2s	⊢ ( 𝑏 ∈ 𝐸 → 𝑏 ∈ ℂ )
13	1	1neven	⊢ 1 ∉ 𝐸
14		elnelne2	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 1 ∉ 𝐸 ) → 𝑏 ≠ 1 )
15	13 14	mpan2	⊢ ( 𝑏 ∈ 𝐸 → 𝑏 ≠ 1 )
16	15	adantr	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → 𝑏 ≠ 1 )
17		simpr	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → 𝑏 ∈ ℂ )
18		2cnd	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → 2 ∈ ℂ )
19		2ne0	⊢ 2 ≠ 0
20	19	a1i	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → 2 ≠ 0 )
21	17 18 20	divcan4d	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( ( 𝑏 · 2 ) / 2 ) = 𝑏 )
22		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
23		divid	⊢ ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 / 2 ) = 1 )
24	22 23	mp1i	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( 2 / 2 ) = 1 )
25	16 21 24	3netr4d	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( ( 𝑏 · 2 ) / 2 ) ≠ ( 2 / 2 ) )
26	17 18	mulcld	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( 𝑏 · 2 ) ∈ ℂ )
27	22	a1i	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
28		div11	⊢ ( ( ( 𝑏 · 2 ) ∈ ℂ ∧ 2 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( 𝑏 · 2 ) / 2 ) = ( 2 / 2 ) ↔ ( 𝑏 · 2 ) = 2 ) )
29	26 18 27 28	syl3anc	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( ( ( 𝑏 · 2 ) / 2 ) = ( 2 / 2 ) ↔ ( 𝑏 · 2 ) = 2 ) )
30	29	biimprd	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( ( 𝑏 · 2 ) = 2 → ( ( 𝑏 · 2 ) / 2 ) = ( 2 / 2 ) ) )
31	30	necon3d	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( ( ( 𝑏 · 2 ) / 2 ) ≠ ( 2 / 2 ) → ( 𝑏 · 2 ) ≠ 2 ) )
32	25 31	mpd	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → ( 𝑏 · 2 ) ≠ 2 )
33	12 32	mpdan	⊢ ( 𝑏 ∈ 𝐸 → ( 𝑏 · 2 ) ≠ 2 )
34	5 9 33	rspcedvd	⊢ ( 𝑏 ∈ 𝐸 → ∃ 𝑎 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎 )
35	34	rgen	⊢ ∀ 𝑏 ∈ 𝐸 ∃ 𝑎 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎