Description: If a unit element lies in the kernel of a ring homomorphism, then 0 = 1 , i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | kerunit.1 | |
|
kerunit.2 | |
||
kerunit.3 | |
||
Assertion | kerunit | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kerunit.1 | |
|
2 | kerunit.2 | |
|
3 | kerunit.3 | |
|
4 | elin | |
|
5 | 4 | biimpi | |
6 | 5 | adantl | |
7 | 6 | simpld | |
8 | rhmrcl1 | |
|
9 | eqid | |
|
10 | eqid | |
|
11 | eqid | |
|
12 | 1 9 10 11 | unitlinv | |
13 | 12 | fveq2d | |
14 | 8 13 | sylan | |
15 | 7 14 | syldan | |
16 | simpl | |
|
17 | 8 | adantr | |
18 | eqid | |
|
19 | 1 9 18 | ringinvcl | |
20 | 17 7 19 | syl2anc | |
21 | 18 1 | unitcl | |
22 | 7 21 | syl | |
23 | eqid | |
|
24 | 18 10 23 | rhmmul | |
25 | 16 20 22 24 | syl3anc | |
26 | 6 | simprd | |
27 | eqid | |
|
28 | 18 27 | rhmf | |
29 | ffn | |
|
30 | elpreima | |
|
31 | 28 29 30 | 3syl | |
32 | 31 | simplbda | |
33 | 26 32 | syldan | |
34 | fvex | |
|
35 | 34 | elsn | |
36 | 33 35 | sylib | |
37 | 36 | oveq2d | |
38 | rhmrcl2 | |
|
39 | 38 | adantr | |
40 | 28 | adantr | |
41 | 40 20 | ffvelrnd | |
42 | 27 23 2 | ringrz | |
43 | 39 41 42 | syl2anc | |
44 | 25 37 43 | 3eqtrd | |
45 | 11 3 | rhm1 | |
46 | 45 | adantr | |
47 | 15 44 46 | 3eqtr3rd | |
48 | 47 | reximdva0 | |
49 | id | |
|
50 | 49 | rexlimivw | |
51 | 48 50 | syl | |