Theorem rngohomsub

Description: Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011)

	Ref	Expression
Hypotheses	rnghomsub.1	$$⊢G=1^{st}\left(R\right)$$
	rnghomsub.2	$$⊢X=\mathrm{ran}G$$
	rnghomsub.3	$$⊢H={/}_g\left(G\right)$$
	rnghomsub.4	$$⊢J=1^{st}\left(S\right)$$
	rnghomsub.5	$$⊢K={/}_g\left(J\right)$$
Assertion	rngohomsub	Could not format assertion : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		rnghomsub.1	$$⊢G=1^{st}\left(R\right)$$
2		rnghomsub.2	$$⊢X=\mathrm{ran}G$$
3		rnghomsub.3	$$⊢H={/}_g\left(G\right)$$
4		rnghomsub.4	$$⊢J=1^{st}\left(S\right)$$
5		rnghomsub.5	$$⊢K={/}_g\left(J\right)$$
6	1	rngogrpo	$$⊢R\in \mathrm{RingOps}\to G\in \mathrm{GrpOp}$$
7	6	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 |-
8	4	rngogrpo	$$⊢S\in \mathrm{RingOps}\to J\in \mathrm{GrpOp}$$
9	8	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 |-
10	1 4	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 |-
11	7 9 10	3jca	Could not format ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( G e. GrpOp /\ J e. GrpOp /\ F e. ( G GrpOpHom J ) ) ) : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( G e. GrpOp /\ J e. GrpOp /\ F e. ( G GrpOpHom J ) ) ) with typecode |-
12	2 3 5	ghomdiv	$$⊢\left(\left(G\in \mathrm{GrpOp}\wedge J\in \mathrm{GrpOp}\wedge F\in \left(G\mathrm{GrpOpHom}J\right)\right)\wedge \left(A\in X\wedge B\in X\right)\right)\to F\left(AHB\right)=F\left(A\right)KF\left(B\right)$$
13	11 12	sylan	Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A H B ) ) = ( ( F ` A ) K ( F ` B ) ) ) with typecode |-