Metamath Proof Explorer

Theorem rngohomadd

Description: Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011)

Ref Expression
Hypotheses rnghomadd.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
rnghomadd.2 ⊢ 𝑋 = ran 𝐺
rnghomadd.3 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
Assertion rngohomadd ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rnghomadd.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 rnghomadd.2 ⊢ 𝑋 = ran 𝐺
3 rnghomadd.3 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
4 eqid ⊢ ( 2nd ‘ 𝑅 ) = ( 2nd ‘ 𝑅 )
5 eqid ⊢ ( GId ‘ ( 2nd ‘ 𝑅 ) ) = ( GId ‘ ( 2nd ‘ 𝑅 ) )
6 eqid ⊢ ( 2nd ‘ 𝑆 ) = ( 2nd ‘ 𝑆 )
7 eqid ⊢ ran 𝐽 = ran 𝐽
8 eqid ⊢ ( GId ‘ ( 2nd ‘ 𝑆 ) ) = ( GId ‘ ( 2nd ‘ 𝑆 ) )
9 1 4 2 5 3 6 7 8 isrngohom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( 𝐹 : 𝑋 ⟶ ran 𝐽 ∧ ( 𝐹 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
10 9 biimpa ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : 𝑋 ⟶ ran 𝐽 ∧ ( 𝐹 ‘ ( GId ‘ ( 2nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2nd ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
11 10 simp3d ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) )
12 11 3impa ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) )
13 simpl ⊢ ( ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
14 13 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
15 12 14 syl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
16 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) )
17 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
18 17 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
20 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
21 20 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) )
22 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
23 22 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝐵 ) ) )
24 21 23 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ ( 𝐴 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝐵 ) ) ) )
25 19 24 rspc2v ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝐵 ) ) ) )
26 15 25 mpan9 ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐺 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐽 ( 𝐹 ‘ 𝐵 ) ) )