This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isrnghmd

Description: Demonstration of non-unital ring homomorphism. (Contributed by AV, 23-Feb-2020)

Ref Expression
Hypotheses isrnghmd.b 
|- B = ( Base ` R )
isrnghmd.t 
|- .x. = ( .r ` R )
isrnghmd.u 
|- .X. = ( .r ` S )
isrnghmd.r 
|- ( ph -> R e. Rng )
isrnghmd.s 
|- ( ph -> S e. Rng )
isrnghmd.ht 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
isrnghmd.c 
|- C = ( Base ` S )
isrnghmd.p 
|- .+ = ( +g ` R )
isrnghmd.q 
|- .+^ = ( +g ` S )
isrnghmd.f 
|- ( ph -> F : B --> C )
isrnghmd.hp 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
Assertion isrnghmd 
|- ( ph -> F e. ( R RngHom S ) )

Proof

Step Hyp Ref Expression
1 isrnghmd.b 
 |-  B = ( Base ` R )
2 isrnghmd.t 
 |-  .x. = ( .r ` R )
3 isrnghmd.u 
 |-  .X. = ( .r ` S )
4 isrnghmd.r 
 |-  ( ph -> R e. Rng )
5 isrnghmd.s 
 |-  ( ph -> S e. Rng )
6 isrnghmd.ht 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
7 isrnghmd.c 
 |-  C = ( Base ` S )
8 isrnghmd.p 
 |-  .+ = ( +g ` R )
9 isrnghmd.q 
 |-  .+^ = ( +g ` S )
10 isrnghmd.f 
 |-  ( ph -> F : B --> C )
11 isrnghmd.hp 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
12 rngabl 
 |-  ( R e. Rng -> R e. Abel )
13 ablgrp 
 |-  ( R e. Abel -> R e. Grp )
14 4 12 13 3syl 
 |-  ( ph -> R e. Grp )
15 rngabl 
 |-  ( S e. Rng -> S e. Abel )
16 ablgrp 
 |-  ( S e. Abel -> S e. Grp )
17 5 15 16 3syl 
 |-  ( ph -> S e. Grp )
18 1 7 8 9 14 17 10 11 isghmd 
 |-  ( ph -> F e. ( R GrpHom S ) )
19 1 2 3 4 5 6 18 isrnghm2d 
 |-  ( ph -> F e. ( R RngHom S ) )