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

Metamath Proof Explorer

Theorem isrnghm2d

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 ) ) )
isrnghm2d.f 
|- ( ph -> F e. ( R GrpHom S ) )
Assertion isrnghm2d 
|- ( 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 isrnghm2d.f 
 |-  ( ph -> F e. ( R GrpHom S ) )
8 4 5 jca 
 |-  ( ph -> ( R e. Rng /\ S e. Rng ) )
9 6 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
10 7 9 jca 
 |-  ( ph -> ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) )
11 1 2 3 isrnghm 
 |-  ( F e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) )
12 8 10 11 sylanbrc 
 |-  ( ph -> F e. ( R RngHom S ) )