Metamath Proof Explorer

Theorem rngohom1

Description: A ring homomorphism preserves 1 . (Contributed by Jeff Madsen, 24-Jun-2011)

		Ref	Expression
	Hypotheses	rnghom1.1	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
		rnghom1.2	⊢ 𝑈 = ( GId ‘ 𝐻 )
		rnghom1.3	⊢ 𝐾 = ( 2^nd ‘ 𝑆 )
		rnghom1.4	⊢ 𝑉 = ( GId ‘ 𝐾 )
	Assertion	rngohom1	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ 𝑈 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		rnghom1.1	⊢ 𝐻 = ( 2^nd ‘ 𝑅 )
2		rnghom1.2	⊢ 𝑈 = ( GId ‘ 𝐻 )
3		rnghom1.3	⊢ 𝐾 = ( 2^nd ‘ 𝑆 )
4		rnghom1.4	⊢ 𝑉 = ( GId ‘ 𝐾 )
5		eqid	⊢ ( 1^st ‘ 𝑅 ) = ( 1^st ‘ 𝑅 )
6		eqid	⊢ ran ( 1^st ‘ 𝑅 ) = ran ( 1^st ‘ 𝑅 )
7		eqid	⊢ ( 1^st ‘ 𝑆 ) = ( 1^st ‘ 𝑆 )
8		eqid	⊢ ran ( 1^st ‘ 𝑆 ) = ran ( 1^st ‘ 𝑆 )
9	5 1 6 2 7 3 8 4	isrngohom	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( 𝐹 : ran ( 1^st ‘ 𝑅 ) ⟶ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
10	9	biimpa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : ran ( 1^st ‘ 𝑅 ) ⟶ ran ( 1^st ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ ran ( 1^st ‘ 𝑅 ) ∀ 𝑦 ∈ ran ( 1^st ‘ 𝑅 ) ( ( 𝐹 ‘ ( 𝑥 ( 1^st ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 1^st ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) )
11	10	simp2d	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ 𝑈 ) = 𝑉 )
12	11	3impa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 ‘ 𝑈 ) = 𝑉 )