Metamath Proof Explorer

Theorem rngogrphom

Description: A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011)

		Ref	Expression
	Hypotheses	rnggrphom.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
		rnggrphom.2	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
	Assertion	rngogrphom	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		rnggrphom.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		rnggrphom.2	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
3		eqid	⊢ ran 𝐺 = ran 𝐺
4		eqid	⊢ ran 𝐽 = ran 𝐽
5	1 3 2 4	rngohomf	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐹 : ran 𝐺 ⟶ ran 𝐽 )
6	1 3 2	rngohomadd	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
7	6	eqcomd	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
8	7	ralrimivva	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
9	1	rngogrpo	⊢ ( 𝑅 ∈ RingOps → 𝐺 ∈ GrpOp )
10	2	rngogrpo	⊢ ( 𝑆 ∈ RingOps → 𝐽 ∈ GrpOp )
11	3 4	elghomOLD	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐽 ∈ GrpOp ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐽 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
12	9 10 11	syl2an	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐽 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
13	12	3adant3	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → ( 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) ↔ ( 𝐹 : ran 𝐺 ⟶ ran 𝐽 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
14	5 8 13	mpbir2and	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ) → 𝐹 ∈ ( 𝐺 GrpOpHom 𝐽 ) )