Theorem 2zrngnmrid

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

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

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4		eldifsn	⊢ ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ↔ ( 𝑎 ∈ 𝐸 ∧ 𝑎 ≠ 0 ) )
5		eqeq1	⊢ ( 𝑧 = 𝑎 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑎 = ( 2 · 𝑥 ) ) )
6	5	rexbidv	⊢ ( 𝑧 = 𝑎 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
7	6 1	elrab2	⊢ ( 𝑎 ∈ 𝐸 ↔ ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
8		zcn	⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
9	8	adantr	⊢ ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) → 𝑎 ∈ ℂ )
10	7 9	sylbi	⊢ ( 𝑎 ∈ 𝐸 → 𝑎 ∈ ℂ )
11	10	anim1i	⊢ ( ( 𝑎 ∈ 𝐸 ∧ 𝑎 ≠ 0 ) → ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) )
12	4 11	sylbi	⊢ ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) → ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) )
13		eqeq1	⊢ ( 𝑧 = 𝑏 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑏 = ( 2 · 𝑥 ) ) )
14	13	rexbidv	⊢ ( 𝑧 = 𝑏 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
15	14 1	elrab2	⊢ ( 𝑏 ∈ 𝐸 ↔ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
16		zcn	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
17	16	adantr	⊢ ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → 𝑏 ∈ ℂ )
18	15 17	sylbi	⊢ ( 𝑏 ∈ 𝐸 → 𝑏 ∈ ℂ )
19	18	ancli	⊢ ( 𝑏 ∈ 𝐸 → ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) )
20	1	1neven	⊢ 1 ∉ 𝐸
21		elnelne2	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 1 ∉ 𝐸 ) → 𝑏 ≠ 1 )
22	20 21	mpan2	⊢ ( 𝑏 ∈ 𝐸 → 𝑏 ≠ 1 )
23	22	ad2antrl	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → 𝑏 ≠ 1 )
24		simpr	⊢ ( ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) → 𝑏 ∈ ℂ )
25	24	anim2i	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ 𝑏 ∈ ℂ ) )
26		3anass	⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ↔ ( 𝑏 ∈ ℂ ∧ ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ) )
27		ancom	⊢ ( ( 𝑏 ∈ ℂ ∧ ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ) ↔ ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ 𝑏 ∈ ℂ ) )
28	26 27	bitri	⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ↔ ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ 𝑏 ∈ ℂ ) )
29	25 28	sylibr	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) )
30		divcan3	⊢ ( ( 𝑏 ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) → ( ( 𝑎 · 𝑏 ) / 𝑎 ) = 𝑏 )
31	29 30	syl	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( ( 𝑎 · 𝑏 ) / 𝑎 ) = 𝑏 )
32		divid	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) → ( 𝑎 / 𝑎 ) = 1 )
33	32	adantr	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( 𝑎 / 𝑎 ) = 1 )
34	23 31 33	3netr4d	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( ( 𝑎 · 𝑏 ) / 𝑎 ) ≠ ( 𝑎 / 𝑎 ) )
35		simpl	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) → 𝑎 ∈ ℂ )
36		mulcl	⊢ ( ( 𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ ) → ( 𝑎 · 𝑏 ) ∈ ℂ )
37	35 24 36	syl2an	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( 𝑎 · 𝑏 ) ∈ ℂ )
38	35	adantr	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → 𝑎 ∈ ℂ )
39		simpl	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) )
40		div11	⊢ ( ( ( 𝑎 · 𝑏 ) ∈ ℂ ∧ 𝑎 ∈ ℂ ∧ ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ) → ( ( ( 𝑎 · 𝑏 ) / 𝑎 ) = ( 𝑎 / 𝑎 ) ↔ ( 𝑎 · 𝑏 ) = 𝑎 ) )
41	37 38 39 40	syl3anc	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( ( ( 𝑎 · 𝑏 ) / 𝑎 ) = ( 𝑎 / 𝑎 ) ↔ ( 𝑎 · 𝑏 ) = 𝑎 ) )
42	41	biimprd	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( ( 𝑎 · 𝑏 ) = 𝑎 → ( ( 𝑎 · 𝑏 ) / 𝑎 ) = ( 𝑎 / 𝑎 ) ) )
43	42	necon3d	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( ( ( 𝑎 · 𝑏 ) / 𝑎 ) ≠ ( 𝑎 / 𝑎 ) → ( 𝑎 · 𝑏 ) ≠ 𝑎 ) )
44	34 43	mpd	⊢ ( ( ( 𝑎 ∈ ℂ ∧ 𝑎 ≠ 0 ) ∧ ( 𝑏 ∈ 𝐸 ∧ 𝑏 ∈ ℂ ) ) → ( 𝑎 · 𝑏 ) ≠ 𝑎 )
45	12 19 44	syl2an	⊢ ( ( 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∧ 𝑏 ∈ 𝐸 ) → ( 𝑎 · 𝑏 ) ≠ 𝑎 )
46	45	rgen2	⊢ ∀ 𝑎 ∈ ( 𝐸 ∖ { 0 } ) ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ≠ 𝑎