Metamath Proof Explorer

Theorem zrrnghm

Description: The constant mapping to zero is a nonunital ring homomorphism from the zero ring to any nonunital ring. (Contributed by AV, 17-Apr-2020)

Ref Expression
Hypotheses zrrhm.b ⊢ B = Base T
zrrhm.0 ⊢ 0 ˙ = 0 S
zrrhm.h ⊢ H = x ∈ B ⟼ 0 ˙
Assertion zrrnghm ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ T RngHomo S

Proof

Step Hyp Ref Expression
1 zrrhm.b ⊢ B = Base T
2 zrrhm.0 ⊢ 0 ˙ = 0 S
3 zrrhm.h ⊢ H = x ∈ B ⟼ 0 ˙
4 eldifi ⊢ T ∈ Ring ∖ NzRing → T ∈ Ring
5 ringrng ⊢ T ∈ Ring → T ∈ Rng
6 4 5 syl ⊢ T ∈ Ring ∖ NzRing → T ∈ Rng
7 6 anim1i ⊢ T ∈ Ring ∖ NzRing ∧ S ∈ Rng → T ∈ Rng ∧ S ∈ Rng
8 7 ancoms ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → T ∈ Rng ∧ S ∈ Rng
9 rngabl ⊢ S ∈ Rng → S ∈ Abel
10 ablgrp ⊢ S ∈ Abel → S ∈ Grp
11 9 10 syl ⊢ S ∈ Rng → S ∈ Grp
12 11 adantr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → S ∈ Grp
13 ringgrp ⊢ T ∈ Ring → T ∈ Grp
14 4 13 syl ⊢ T ∈ Ring ∖ NzRing → T ∈ Grp
15 14 adantl ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → T ∈ Grp
16 eqid ⊢ 0 T = 0 T
17 1 16 0ringbas ⊢ T ∈ Ring ∖ NzRing → B = 0 T
18 17 adantl ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → B = 0 T
19 1 2 3 16 c0snghm ⊢ S ∈ Grp ∧ T ∈ Grp ∧ B = 0 T → H ∈ T GrpHom S
20 12 15 18 19 syl3anc ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ T GrpHom S
21 3 a1i ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → H = x ∈ B ⟼ 0 ˙
22 eqidd ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ x = 0 T → 0 ˙ = 0 ˙
23 1 16 ring0cl ⊢ T ∈ Ring → 0 T ∈ B
24 4 23 syl ⊢ T ∈ Ring ∖ NzRing → 0 T ∈ B
25 24 ad2antlr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → 0 T ∈ B
26 2 fvexi ⊢ 0 ˙ ∈ V
27 26 a1i ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → 0 ˙ ∈ V
28 21 22 25 27 fvmptd ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → H ⁡ 0 T = 0 ˙
29 eqid ⊢ Base S = Base S
30 29 2 grpidcl ⊢ S ∈ Grp → 0 ˙ ∈ Base S
31 11 30 syl ⊢ S ∈ Rng → 0 ˙ ∈ Base S
32 eqid ⊢ ⋅ S = ⋅ S
33 29 32 2 rnglz ⊢ S ∈ Rng ∧ 0 ˙ ∈ Base S → 0 ˙ ⋅ S 0 ˙ = 0 ˙
34 31 33 mpdan ⊢ S ∈ Rng → 0 ˙ ⋅ S 0 ˙ = 0 ˙
35 34 adantr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → 0 ˙ ⋅ S 0 ˙ = 0 ˙
36 35 adantr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → 0 ˙ ⋅ S 0 ˙ = 0 ˙
37 36 adantr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → 0 ˙ ⋅ S 0 ˙ = 0 ˙
38 simpr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → H ⁡ 0 T = 0 ˙
39 38 38 oveq12d ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → H ⁡ 0 T ⋅ S H ⁡ 0 T = 0 ˙ ⋅ S 0 ˙
40 eqid ⊢ ⋅ T = ⋅ T
41 1 40 16 ringlz ⊢ T ∈ Ring ∧ 0 T ∈ B → 0 T ⋅ T 0 T = 0 T
42 4 23 41 syl2anc2 ⊢ T ∈ Ring ∖ NzRing → 0 T ⋅ T 0 T = 0 T
43 42 ad2antlr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → 0 T ⋅ T 0 T = 0 T
44 43 adantr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → 0 T ⋅ T 0 T = 0 T
45 44 fveq2d ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → H ⁡ 0 T ⋅ T 0 T = H ⁡ 0 T
46 45 38 eqtrd ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → H ⁡ 0 T ⋅ T 0 T = 0 ˙
47 37 39 46 3eqtr4rd ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T ∧ H ⁡ 0 T = 0 ˙ → H ⁡ 0 T ⋅ T 0 T = H ⁡ 0 T ⋅ S H ⁡ 0 T
48 28 47 mpdan ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → H ⁡ 0 T ⋅ T 0 T = H ⁡ 0 T ⋅ S H ⁡ 0 T
49 23 23 jca ⊢ T ∈ Ring → 0 T ∈ B ∧ 0 T ∈ B
50 4 49 syl ⊢ T ∈ Ring ∖ NzRing → 0 T ∈ B ∧ 0 T ∈ B
51 50 ad2antlr ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → 0 T ∈ B ∧ 0 T ∈ B
52 fvoveq1 ⊢ a = 0 T → H ⁡ a ⋅ T c = H ⁡ 0 T ⋅ T c
53 fveq2 ⊢ a = 0 T → H ⁡ a = H ⁡ 0 T
54 53 oveq1d ⊢ a = 0 T → H ⁡ a ⋅ S H ⁡ c = H ⁡ 0 T ⋅ S H ⁡ c
55 52 54 eqeq12d ⊢ a = 0 T → H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c ↔ H ⁡ 0 T ⋅ T c = H ⁡ 0 T ⋅ S H ⁡ c
56 oveq2 ⊢ c = 0 T → 0 T ⋅ T c = 0 T ⋅ T 0 T
57 56 fveq2d ⊢ c = 0 T → H ⁡ 0 T ⋅ T c = H ⁡ 0 T ⋅ T 0 T
58 fveq2 ⊢ c = 0 T → H ⁡ c = H ⁡ 0 T
59 58 oveq2d ⊢ c = 0 T → H ⁡ 0 T ⋅ S H ⁡ c = H ⁡ 0 T ⋅ S H ⁡ 0 T
60 57 59 eqeq12d ⊢ c = 0 T → H ⁡ 0 T ⋅ T c = H ⁡ 0 T ⋅ S H ⁡ c ↔ H ⁡ 0 T ⋅ T 0 T = H ⁡ 0 T ⋅ S H ⁡ 0 T
61 55 60 2ralsng ⊢ 0 T ∈ B ∧ 0 T ∈ B → ∀ a ∈ 0 T ∀ c ∈ 0 T H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c ↔ H ⁡ 0 T ⋅ T 0 T = H ⁡ 0 T ⋅ S H ⁡ 0 T
62 51 61 syl ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → ∀ a ∈ 0 T ∀ c ∈ 0 T H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c ↔ H ⁡ 0 T ⋅ T 0 T = H ⁡ 0 T ⋅ S H ⁡ 0 T
63 48 62 mpbird ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → ∀ a ∈ 0 T ∀ c ∈ 0 T H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
64 raleq ⊢ B = 0 T → ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c ↔ ∀ c ∈ 0 T H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
65 64 raleqbi1dv ⊢ B = 0 T → ∀ a ∈ B ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c ↔ ∀ a ∈ 0 T ∀ c ∈ 0 T H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
66 65 adantl ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → ∀ a ∈ B ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c ↔ ∀ a ∈ 0 T ∀ c ∈ 0 T H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
67 63 66 mpbird ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing ∧ B = 0 T → ∀ a ∈ B ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
68 18 67 mpdan ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → ∀ a ∈ B ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
69 20 68 jca ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ T GrpHom S ∧ ∀ a ∈ B ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
70 1 40 32 isrnghm ⊢ H ∈ T RngHomo S ↔ T ∈ Rng ∧ S ∈ Rng ∧ H ∈ T GrpHom S ∧ ∀ a ∈ B ∀ c ∈ B H ⁡ a ⋅ T c = H ⁡ a ⋅ S H ⁡ c
71 8 69 70 sylanbrc ⊢ S ∈ Rng ∧ T ∈ Ring ∖ NzRing → H ∈ T RngHomo S