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

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

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 ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐺 ∈ GrpOp )
8 4 rngogrpo ⊢ ( 𝑆 ∈ RingOps → 𝐽 ∈ GrpOp )
9 8 3ad2ant2 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐽 ∈ GrpOp )
10 1 4 rngogrphom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) )
11 7 9 10 3jca ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ) )
12 2 3 5 ghomdiv ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ∧ 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )
13 11 12 sylan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )