Metamath Proof Explorer


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 𝑆 ) ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹𝐴 ) 𝐾 ( 𝐹𝐵 ) ) )