Metamath Proof Explorer

Theorem rngohommul

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

Ref Expression
Hypotheses rnghommul.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
rnghommul.2 ⊢ 𝑋 = ran 𝐺
rnghommul.3 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
rnghommul.4 ⊢ 𝐾 = ( 2nd ‘ 𝑆 )
Assertion rngohommul ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rnghommul.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 rnghommul.2 ⊢ 𝑋 = ran 𝐺
3 rnghommul.3 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
4 rnghommul.4 ⊢ 𝐾 = ( 2nd ‘ 𝑆 )
5 eqid ⊢ ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
6 eqid ⊢ ( 1st ‘ 𝑆 ) = ( 1st ‘ 𝑆 )
7 eqid ⊢ ran ( 1st ‘ 𝑆 ) = ran ( 1st ‘ 𝑆 )
8 eqid ⊢ ( GId ‘ 𝐾 ) = ( GId ‘ 𝐾 )
9 1 3 2 5 6 4 7 8 isrngohom ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( 𝐹 : 𝑋 ⟶ ran ( 1st ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( GId ‘ 𝐻 ) ) = ( GId ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
10 9 biimpa ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : 𝑋 ⟶ ran ( 1st ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( GId ‘ 𝐻 ) ) = ( GId ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) )
11 10 simp3d ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) )
12 11 3impa ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) )
13 simpr ⊢ ( ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
14 13 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
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 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )