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=mulGrpR
Assertion 2zrngnmrid ⊢∀a∈E∖0∀b∈Ea⁢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=mulGrpR
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⁢ba=b
31 29 30 syl ⊢a∈ℂ∧a≠0∧b∈E∧b∈ℂ→a⁢ba=b
32 divid ⊢a∈ℂ∧a≠0→aa=1
33 32 adantr ⊢a∈ℂ∧a≠0∧b∈E∧b∈ℂ→aa=1
34 23 31 33 3netr4d ⊢a∈ℂ∧a≠0∧b∈E∧b∈ℂ→a⁢ba≠aa
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⁢ba=aa↔a⁢b=a
41 37 38 39 40 syl3anc ⊢a∈ℂ∧a≠0∧b∈E∧b∈ℂ→a⁢ba=aa↔a⁢b=a
42 41 biimprd ⊢a∈ℂ∧a≠0∧b∈E∧b∈ℂ→a⁢b=a→a⁢ba=aa
43 42 necon3d ⊢a∈ℂ∧a≠0∧b∈E∧b∈ℂ→a⁢ba≠aa→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∈Ea⁢b≠a