Theorem 2zrngnmlid2

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	2zrngnmlid2	⊢ ∀ 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4	1 2 3	2zrngnmrid	⊢ ∀ 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ≠ 𝑎
5		eldifi	⊢ ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) → 𝑎 ∈ 𝐸 )
6		elrabi	⊢ ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑎 ∈ ℤ )
7	6	zcnd	⊢ ( 𝑎 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑎 ∈ ℂ )
8	7 1	eleq2s	⊢ ( 𝑎 ∈ 𝐸 → 𝑎 ∈ ℂ )
9	5 8	syl	⊢ ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) → 𝑎 ∈ ℂ )
10		elrabi	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℤ )
11	10	zcnd	⊢ ( 𝑏 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑏 ∈ ℂ )
12	11 1	eleq2s	⊢ ( 𝑏 ∈ 𝐸 → 𝑏 ∈ ℂ )
13		mulcom	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑎 · 𝑏 ) = ( 𝑏 · 𝑎 ) )
14	9 12 13	syl2an	⊢ ( ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐸 ) → ( 𝑎 · 𝑏 ) = ( 𝑏 · 𝑎 ) )
15	14	eqcomd	⊢ ( ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐸 ) → ( 𝑏 · 𝑎 ) = ( 𝑎 · 𝑏 ) )
16	15	eqeq1d	⊢ ( ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐸 ) → ( ( 𝑏 · 𝑎 ) = 𝑎 ↔ ( 𝑎 · 𝑏 ) = 𝑎 ) )
17	16	biimpd	⊢ ( ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐸 ) → ( ( 𝑏 · 𝑎 ) = 𝑎 → ( 𝑎 · 𝑏 ) = 𝑎 ) )
18	17	necon3d	⊢ ( ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐸 ) → ( ( 𝑎 · 𝑏 ) ≠ 𝑎 → ( 𝑏 · 𝑎 ) ≠ 𝑎 ) )
19	18	ralimdva	⊢ ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) → ( ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ≠ 𝑎 → ∀ 𝑏 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎 ) )
20	19	ralimia	⊢ ( ∀ 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ≠ 𝑎 → ∀ 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎 )
21	4 20	ax-mp	⊢ ∀ 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐸 ( 𝑏 · 𝑎 ) ≠ 𝑎