rngohomval

Description: The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 22-Sep-2015)

	Ref	Expression
Hypotheses	rnghomval.1	$⊢ G = 1^{st} (R)$
	rnghomval.2	$⊢ H = 2^{nd} (R)$
	rnghomval.3	$⊢ X = ran G$
	rnghomval.4	$⊢ U = GId (H)$
	rnghomval.5	$⊢ J = 1^{st} (S)$
	rnghomval.6	$⊢ K = 2^{nd} (S)$
	rnghomval.7	$⊢ Y = ran J$
	rnghomval.8	$⊢ V = GId (K)$
Assertion	rngohomval	$⊢ (R \in RingOps \land S \in RingOps) \to R RngHom S = \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\}$

Proof

Step	Hyp	Ref	Expression
1		rnghomval.1	$⊢ G = 1^{st} (R)$
2		rnghomval.2	$⊢ H = 2^{nd} (R)$
3		rnghomval.3	$⊢ X = ran G$
4		rnghomval.4	$⊢ U = GId (H)$
5		rnghomval.5	$⊢ J = 1^{st} (S)$
6		rnghomval.6	$⊢ K = 2^{nd} (S)$
7		rnghomval.7	$⊢ Y = ran J$
8		rnghomval.8	$⊢ V = GId (K)$
9		simpr	$⊢ (r = R \land s = S) \to s = S$
10	9	fveq2d	$⊢ (r = R \land s = S) \to 1^{st} (s) = 1^{st} (S)$
11	10 5	syl6eqr	$⊢ (r = R \land s = S) \to 1^{st} (s) = J$
12	11	rneqd	$⊢ (r = R \land s = S) \to ran 1^{st} (s) = ran J$
13	12 7	syl6eqr	$⊢ (r = R \land s = S) \to ran 1^{st} (s) = Y$
14		simpl	$⊢ (r = R \land s = S) \to r = R$
15	14	fveq2d	$⊢ (r = R \land s = S) \to 1^{st} (r) = 1^{st} (R)$
16	15 1	syl6eqr	$⊢ (r = R \land s = S) \to 1^{st} (r) = G$
17	16	rneqd	$⊢ (r = R \land s = S) \to ran 1^{st} (r) = ran G$
18	17 3	syl6eqr	$⊢ (r = R \land s = S) \to ran 1^{st} (r) = X$
19	13 18	oveq12d	$⊢ (r = R \land s = S) \to {ran 1^{st} (s)}^{ran 1^{st} (r)} = Y^{X}$
20	14	fveq2d	$⊢ (r = R \land s = S) \to 2^{nd} (r) = 2^{nd} (R)$
21	20 2	syl6eqr	$⊢ (r = R \land s = S) \to 2^{nd} (r) = H$
22	21	fveq2d	$⊢ (r = R \land s = S) \to GId (2^{nd} (r)) = GId (H)$
23	22 4	syl6eqr	$⊢ (r = R \land s = S) \to GId (2^{nd} (r)) = U$
24	23	fveq2d	$⊢ (r = R \land s = S) \to f (GId (2^{nd} (r))) = f (U)$
25	9	fveq2d	$⊢ (r = R \land s = S) \to 2^{nd} (s) = 2^{nd} (S)$
26	25 6	syl6eqr	$⊢ (r = R \land s = S) \to 2^{nd} (s) = K$
27	26	fveq2d	$⊢ (r = R \land s = S) \to GId (2^{nd} (s)) = GId (K)$
28	27 8	syl6eqr	$⊢ (r = R \land s = S) \to GId (2^{nd} (s)) = V$
29	24 28	eqeq12d	$⊢ (r = R \land s = S) \to (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \leftrightarrow f (U) = V)$
30	16	oveqd	$⊢ (r = R \land s = S) \to x 1^{st} (r) y = x G y$
31	30	fveq2d	$⊢ (r = R \land s = S) \to f (x 1^{st} (r) y) = f (x G y)$
32	11	oveqd	$⊢ (r = R \land s = S) \to f (x) 1^{st} (s) f (y) = f (x) J f (y)$
33	31 32	eqeq12d	$⊢ (r = R \land s = S) \to (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \leftrightarrow f (x G y) = f (x) J f (y))$
34	21	oveqd	$⊢ (r = R \land s = S) \to x 2^{nd} (r) y = x H y$
35	34	fveq2d	$⊢ (r = R \land s = S) \to f (x 2^{nd} (r) y) = f (x H y)$
36	26	oveqd	$⊢ (r = R \land s = S) \to f (x) 2^{nd} (s) f (y) = f (x) K f (y)$
37	35 36	eqeq12d	$⊢ (r = R \land s = S) \to (f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y) \leftrightarrow f (x H y) = f (x) K f (y))$
38	33 37	anbi12d	$⊢ (r = R \land s = S) \to ((f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)) \leftrightarrow (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))$
39	18 38	raleqbidv	$⊢ (r = R \land s = S) \to (\forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)) \leftrightarrow \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))$
40	18 39	raleqbidv	$⊢ (r = R \land s = S) \to (\forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)) \leftrightarrow \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))$
41	29 40	anbi12d	$⊢ (r = R \land s = S) \to ((f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y))) \leftrightarrow (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y))))$
42	19 41	rabeqbidv	$⊢ (r = R \land s = S) \to \{f \in ({ran 1^{st} (s)}^{ran 1^{st} (r)}) \| (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))\} = \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\}$
43		df-rngohom	$⊢ RngHom = (r \in RingOps, s \in RingOps ⟼ \{f \in ({ran 1^{st} (s)}^{ran 1^{st} (r)}) \| (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))\})$
44		ovex	$⊢ Y^{X} \in V$
45	44	rabex	$⊢ \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\} \in V$
46	42 43 45	ovmpoa	$⊢ (R \in RingOps \land S \in RingOps) \to R RngHom S = \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\}$

Metamath Proof Explorer

Theorem rngohomval

Proof