Metamath Proof Explorer


Theorem kerunit

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 U=UnitR
kerunit.2 0˙=0S
kerunit.3 1˙=1S
Assertion kerunit FRRingHomSUF-10˙1˙=0˙

Proof

Step Hyp Ref Expression
1 kerunit.1 U=UnitR
2 kerunit.2 0˙=0S
3 kerunit.3 1˙=1S
4 elin xUF-10˙xUxF-10˙
5 4 biimpi xUF-10˙xUxF-10˙
6 5 adantl FRRingHomSxUF-10˙xUxF-10˙
7 6 simpld FRRingHomSxUF-10˙xU
8 rhmrcl1 FRRingHomSRRing
9 eqid invrR=invrR
10 eqid R=R
11 eqid 1R=1R
12 1 9 10 11 unitlinv RRingxUinvrRxRx=1R
13 12 fveq2d RRingxUFinvrRxRx=F1R
14 8 13 sylan FRRingHomSxUFinvrRxRx=F1R
15 7 14 syldan FRRingHomSxUF-10˙FinvrRxRx=F1R
16 simpl FRRingHomSxUF-10˙FRRingHomS
17 8 adantr FRRingHomSxUF-10˙RRing
18 eqid BaseR=BaseR
19 1 9 18 ringinvcl RRingxUinvrRxBaseR
20 17 7 19 syl2anc FRRingHomSxUF-10˙invrRxBaseR
21 18 1 unitcl xUxBaseR
22 7 21 syl FRRingHomSxUF-10˙xBaseR
23 eqid S=S
24 18 10 23 rhmmul FRRingHomSinvrRxBaseRxBaseRFinvrRxRx=FinvrRxSFx
25 16 20 22 24 syl3anc FRRingHomSxUF-10˙FinvrRxRx=FinvrRxSFx
26 6 simprd FRRingHomSxUF-10˙xF-10˙
27 eqid BaseS=BaseS
28 18 27 rhmf FRRingHomSF:BaseRBaseS
29 ffn F:BaseRBaseSFFnBaseR
30 elpreima FFnBaseRxF-10˙xBaseRFx0˙
31 28 29 30 3syl FRRingHomSxF-10˙xBaseRFx0˙
32 31 simplbda FRRingHomSxF-10˙Fx0˙
33 26 32 syldan FRRingHomSxUF-10˙Fx0˙
34 fvex FxV
35 34 elsn Fx0˙Fx=0˙
36 33 35 sylib FRRingHomSxUF-10˙Fx=0˙
37 36 oveq2d FRRingHomSxUF-10˙FinvrRxSFx=FinvrRxS0˙
38 rhmrcl2 FRRingHomSSRing
39 38 adantr FRRingHomSxUF-10˙SRing
40 28 adantr FRRingHomSxUF-10˙F:BaseRBaseS
41 40 20 ffvelrnd FRRingHomSxUF-10˙FinvrRxBaseS
42 27 23 2 ringrz SRingFinvrRxBaseSFinvrRxS0˙=0˙
43 39 41 42 syl2anc FRRingHomSxUF-10˙FinvrRxS0˙=0˙
44 25 37 43 3eqtrd FRRingHomSxUF-10˙FinvrRxRx=0˙
45 11 3 rhm1 FRRingHomSF1R=1˙
46 45 adantr FRRingHomSxUF-10˙F1R=1˙
47 15 44 46 3eqtr3rd FRRingHomSxUF-10˙1˙=0˙
48 47 reximdva0 FRRingHomSUF-10˙xUF-10˙1˙=0˙
49 id 1˙=0˙1˙=0˙
50 49 rexlimivw xUF-10˙1˙=0˙1˙=0˙
51 48 50 syl FRRingHomSUF-10˙1˙=0˙