Theorem rngohommul

Description: Obsolete theorem, use rhmmul instead. Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

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 ) → ( 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ↔ ( 𝐹 : 𝑋 ⟶ ran ( 1st ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( GId ‘ 𝐻 ) ) = ( GId ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
10	9	biimpa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ( 𝐹 : 𝑋 ⟶ ran ( 1st ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( GId ‘ 𝐻 ) ) = ( GId ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) )
11	10	simp3d	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) )
12	11	3impa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) )
13		simpr	⊢ ( ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
14	13	2ralimi	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
15	12 14	syl	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
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 ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝐾 ( 𝐹 ‘ 𝐵 ) ) )