Theorem rngohom0

Description: A ring homomorphism preserves 0 . (Contributed by Jeff Madsen, 2-Jan-2011)

	Ref	Expression
Hypotheses	rnghom0.1	$$⊢G=1^{st}\left(R\right)$$
	rnghom0.2	$$⊢Z=\mathrm{GId}\left(G\right)$$
	rnghom0.3	$$⊢J=1^{st}\left(S\right)$$
	rnghom0.4	$$⊢W=\mathrm{GId}\left(J\right)$$
Assertion	rngohom0	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` Z ) = W ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rnghom0.1	$$⊢G=1^{st}\left(R\right)$$
2		rnghom0.2	$$⊢Z=\mathrm{GId}\left(G\right)$$
3		rnghom0.3	$$⊢J=1^{st}\left(S\right)$$
4		rnghom0.4	$$⊢W=\mathrm{GId}\left(J\right)$$
5	1	rngogrpo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$
6	5	3ad2ant1	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> G e. GrpOp ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> G e. GrpOp ) with typecode |-
7	3	rngogrpo	$$⊢S\in \mathrm{RingOps}\to J\in \mathrm{GrpOp}$$
8	7	3ad2ant2	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> J e. GrpOp ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> J e. GrpOp ) with typecode |-
9	1 3	rngogrphom	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( G GrpOpHom J ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> F e. ( G GrpOpHom J ) ) with typecode |-
10	2 4	ghomidOLD	$$⊢\left(G\in \mathrm{GrpOp}\wedge J\in \mathrm{GrpOp}\wedge F\in \left(G\mathrm{GrpOpHom}J\right)\right)\to F\left(Z\right)=W$$
11	6 8 9 10	syl3anc	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` Z ) = W ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( F ` Z ) = W ) with typecode |-