Metamath Proof Explorer

Theorem zrrnghm

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

Ref Expression
Hypotheses zrrnghm.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
zrrnghm.0 ⊢ 0 = ( 0g ‘ 𝑆 )
zrrnghm.h ⊢ 𝐻 = ( 𝑥 ∈ 𝐵 ↦ 0 )
Assertion zrrnghm ( ( 𝑆 ∈ Rng ∧ 𝑇 ∈ ( Ring ∖ NzRing ) ) → 𝐻 ∈ ( 𝑇 RngHom 𝑆 ) )

Proof

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