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	$⊢ φ \to B = {Base}_{K}$
	zrhpropd.2	$⊢ φ \to B = {Base}_{L}$
	zrhpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	zrhpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
Assertion	zrhpropd	$⊢ φ \to ℤRHom (K) = ℤRHom (L)$

Step	Hyp	Ref	Expression
1		zrhpropd.1	$⊢ φ \to B = {Base}_{K}$
2		zrhpropd.2	$⊢ φ \to B = {Base}_{L}$
3		zrhpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		zrhpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5		eqidd	$⊢ φ \to {Base}_{ℤ_{ring}} = {Base}_{ℤ_{ring}}$
6		eqidd	$⊢ (φ \land (x \in {Base}_{ℤ_{ring}} \land y \in {Base}_{ℤ_{ring}})) \to x +_{ℤ_{ring}} y = x +_{ℤ_{ring}} y$
7		eqidd	$⊢ (φ \land (x \in {Base}_{ℤ_{ring}} \land y \in {Base}_{ℤ_{ring}})) \to x \cdot_{ℤ_{ring}} y = x \cdot_{ℤ_{ring}} y$
8	5 1 5 2 6 3 7 4	rhmpropd	$⊢ φ \to ℤ_{ring} RingHom K = ℤ_{ring} RingHom L$
9	8	unieqd	$⊢ φ \to ⋃ (ℤ_{ring} RingHom K) = ⋃ (ℤ_{ring} RingHom L)$
10		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
11	10	zrhval	$⊢ ℤRHom (K) = ⋃ (ℤ_{ring} RingHom K)$
12		eqid	$⊢ ℤRHom (L) = ℤRHom (L)$
13	12	zrhval	$⊢ ℤRHom (L) = ⋃ (ℤ_{ring} RingHom L)$
14	9 11 13	3eqtr4g	$⊢ φ \to ℤRHom (K) = ℤRHom (L)$

Metamath Proof Explorer