Theorem rngohomsub

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

	Ref	Expression
Hypotheses	rnghomsub.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	rnghomsub.2	⊢ 𝑋 = ran 𝐺
	rnghomsub.3	⊢ 𝐻 = ( /𝑔 ‘ 𝐺 )
	rnghomsub.4	⊢ 𝐽 = ( 1st ‘ 𝑆 )
	rnghomsub.5	⊢ 𝐾 = ( /𝑔 ‘ 𝐽 )
Assertion	rngohomsub	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rnghomsub.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		rnghomsub.2	⊢ 𝑋 = ran 𝐺
3		rnghomsub.3	⊢ 𝐻 = ( /𝑔 ‘ 𝐺 )
4		rnghomsub.4	⊢ 𝐽 = ( 1st ‘ 𝑆 )
5		rnghomsub.5	⊢ 𝐾 = ( /𝑔 ‘ 𝐽 )
6	1	rngogrpo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
7	6	3ad2ant1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐺 ∈ GrpOp )
8	4	rngogrpo	⊢ ( 𝑆 ∈ RingOps → 𝐽 ∈ GrpOp )
9	8	3ad2ant2	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐽 ∈ GrpOp )
10	1 4	rngogrphom	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) )
11	7 9 10	3jca	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ) )
12	2 3 5	ghomdiv	⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )
13	11 12	sylan	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )