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 = Unit R
kerunit.2 0 ˙ = 0 S
kerunit.3 1 ˙ = 1 S
Assertion kerunit F R RingHom S U F -1 0 ˙ 1 ˙ = 0 ˙

Proof

Step Hyp Ref Expression
1 kerunit.1 U = Unit R
2 kerunit.2 0 ˙ = 0 S
3 kerunit.3 1 ˙ = 1 S
4 elin x U F -1 0 ˙ x U x F -1 0 ˙
5 4 biimpi x U F -1 0 ˙ x U x F -1 0 ˙
6 5 adantl F R RingHom S x U F -1 0 ˙ x U x F -1 0 ˙
7 6 simpld F R RingHom S x U F -1 0 ˙ x U
8 rhmrcl1 F R RingHom S R Ring
9 eqid inv r R = inv r R
10 eqid R = R
11 eqid 1 R = 1 R
12 1 9 10 11 unitlinv R Ring x U inv r R x R x = 1 R
13 12 fveq2d R Ring x U F inv r R x R x = F 1 R
14 8 13 sylan F R RingHom S x U F inv r R x R x = F 1 R
15 7 14 syldan F R RingHom S x U F -1 0 ˙ F inv r R x R x = F 1 R
16 simpl F R RingHom S x U F -1 0 ˙ F R RingHom S
17 8 adantr F R RingHom S x U F -1 0 ˙ R Ring
18 eqid Base R = Base R
19 1 9 18 ringinvcl R Ring x U inv r R x Base R
20 17 7 19 syl2anc F R RingHom S x U F -1 0 ˙ inv r R x Base R
21 18 1 unitcl x U x Base R
22 7 21 syl F R RingHom S x U F -1 0 ˙ x Base R
23 eqid S = S
24 18 10 23 rhmmul F R RingHom S inv r R x Base R x Base R F inv r R x R x = F inv r R x S F x
25 16 20 22 24 syl3anc F R RingHom S x U F -1 0 ˙ F inv r R x R x = F inv r R x S F x
26 6 simprd F R RingHom S x U F -1 0 ˙ x F -1 0 ˙
27 eqid Base S = Base S
28 18 27 rhmf F R RingHom S F : Base R Base S
29 ffn F : Base R Base S F Fn Base R
30 elpreima F Fn Base R x F -1 0 ˙ x Base R F x 0 ˙
31 28 29 30 3syl F R RingHom S x F -1 0 ˙ x Base R F x 0 ˙
32 31 simplbda F R RingHom S x F -1 0 ˙ F x 0 ˙
33 26 32 syldan F R RingHom S x U F -1 0 ˙ F x 0 ˙
34 fvex F x V
35 34 elsn F x 0 ˙ F x = 0 ˙
36 33 35 sylib F R RingHom S x U F -1 0 ˙ F x = 0 ˙
37 36 oveq2d F R RingHom S x U F -1 0 ˙ F inv r R x S F x = F inv r R x S 0 ˙
38 rhmrcl2 F R RingHom S S Ring
39 38 adantr F R RingHom S x U F -1 0 ˙ S Ring
40 28 adantr F R RingHom S x U F -1 0 ˙ F : Base R Base S
41 40 20 ffvelrnd F R RingHom S x U F -1 0 ˙ F inv r R x Base S
42 27 23 2 ringrz S Ring F inv r R x Base S F inv r R x S 0 ˙ = 0 ˙
43 39 41 42 syl2anc F R RingHom S x U F -1 0 ˙ F inv r R x S 0 ˙ = 0 ˙
44 25 37 43 3eqtrd F R RingHom S x U F -1 0 ˙ F inv r R x R x = 0 ˙
45 11 3 rhm1 F R RingHom S F 1 R = 1 ˙
46 45 adantr F R RingHom S x U F -1 0 ˙ F 1 R = 1 ˙
47 15 44 46 3eqtr3rd F R RingHom S x U F -1 0 ˙ 1 ˙ = 0 ˙
48 47 reximdva0 F R RingHom S U F -1 0 ˙ x U F -1 0 ˙ 1 ˙ = 0 ˙
49 id 1 ˙ = 0 ˙ 1 ˙ = 0 ˙
50 49 rexlimivw x U F -1 0 ˙ 1 ˙ = 0 ˙ 1 ˙ = 0 ˙
51 48 50 syl F R RingHom S U F -1 0 ˙ 1 ˙ = 0 ˙