Theorem zrhpropd

Description: The ZZ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	zrhpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	zrhpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
	zrhpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
	zrhpropd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
Assertion	zrhpropd	⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		zrhpropd.1	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		zrhpropd.2	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐿 ) )
3		zrhpropd.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝐿 ) 𝑦 ) )
4		zrhpropd.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝐾 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐿 ) 𝑦 ) )
5		eqidd	⊢ ( 𝜑 → ( Base ‘ ℤring ) = ( Base ‘ ℤring ) )
6		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ℤring ) ∧ 𝑦 ∈ ( Base ‘ ℤring ) ) ) → ( 𝑥 ( +g ‘ ℤring ) 𝑦 ) = ( 𝑥 ( +g ‘ ℤring ) 𝑦 ) )
7		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ℤring ) ∧ 𝑦 ∈ ( Base ‘ ℤring ) ) ) → ( 𝑥 ( .r ‘ ℤring ) 𝑦 ) = ( 𝑥 ( .r ‘ ℤring ) 𝑦 ) )
8	5 1 5 2 6 3 7 4	rhmpropd	⊢ ( 𝜑 → ( ℤring RingHom 𝐾 ) = ( ℤring RingHom 𝐿 ) )
9	8	unieqd	⊢ ( 𝜑 → ∪ ( ℤring RingHom 𝐾 ) = ∪ ( ℤring RingHom 𝐿 ) )
10		eqid	⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
11	10	zrhval	⊢ ( ℤRHom ‘ 𝐾 ) = ∪ ( ℤring RingHom 𝐾 )
12		eqid	⊢ ( ℤRHom ‘ 𝐿 ) = ( ℤRHom ‘ 𝐿 )
13	12	zrhval	⊢ ( ℤRHom ‘ 𝐿 ) = ∪ ( ℤring RingHom 𝐿 )
14	9 11 13	3eqtr4g	⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐿 ) )