Metamath Proof Explorer


Theorem 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 RingOps S RingOps R RngHom S = f Y X | f U = V x X y X f x G y = f x J f y 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 s = S s = S
10 9 fveq2d r = R s = S 1 st s = 1 st S
11 10 5 eqtr4di r = R s = S 1 st s = J
12 11 rneqd r = R s = S ran 1 st s = ran J
13 12 7 eqtr4di r = R s = S ran 1 st s = Y
14 simpl r = R s = S r = R
15 14 fveq2d r = R s = S 1 st r = 1 st R
16 15 1 eqtr4di r = R s = S 1 st r = G
17 16 rneqd r = R s = S ran 1 st r = ran G
18 17 3 eqtr4di r = R s = S ran 1 st r = X
19 13 18 oveq12d r = R s = S ran 1 st s ran 1 st r = Y X
20 14 fveq2d r = R s = S 2 nd r = 2 nd R
21 20 2 eqtr4di r = R s = S 2 nd r = H
22 21 fveq2d r = R s = S GId 2 nd r = GId H
23 22 4 eqtr4di r = R s = S GId 2 nd r = U
24 23 fveq2d r = R s = S f GId 2 nd r = f U
25 9 fveq2d r = R s = S 2 nd s = 2 nd S
26 25 6 eqtr4di r = R s = S 2 nd s = K
27 26 fveq2d r = R s = S GId 2 nd s = GId K
28 27 8 eqtr4di r = R s = S GId 2 nd s = V
29 24 28 eqeq12d r = R s = S f GId 2 nd r = GId 2 nd s f U = V
30 16 oveqd r = R s = S x 1 st r y = x G y
31 30 fveq2d r = R s = S f x 1 st r y = f x G y
32 11 oveqd r = R s = S f x 1 st s f y = f x J f y
33 31 32 eqeq12d r = R s = S f x 1 st r y = f x 1 st s f y f x G y = f x J f y
34 21 oveqd r = R s = S x 2 nd r y = x H y
35 34 fveq2d r = R s = S f x 2 nd r y = f x H y
36 26 oveqd r = R s = S f x 2 nd s f y = f x K f y
37 35 36 eqeq12d r = R s = S f x 2 nd r y = f x 2 nd s f y f x H y = f x K f y
38 33 37 anbi12d r = R s = S f x 1 st r y = f x 1 st s f y f x 2 nd r y = f x 2 nd s f y f x G y = f x J f y f x H y = f x K f y
39 18 38 raleqbidv r = R s = S y ran 1 st r f x 1 st r y = f x 1 st s f y f x 2 nd r y = f x 2 nd s f y y X f x G y = f x J f y f x H y = f x K f y
40 18 39 raleqbidv r = R s = S x ran 1 st r y ran 1 st r f x 1 st r y = f x 1 st s f y f x 2 nd r y = f x 2 nd s f y x X y X f x G y = f x J f y f x H y = f x K f y
41 29 40 anbi12d r = R s = S f GId 2 nd r = GId 2 nd s x ran 1 st r y ran 1 st r f x 1 st r y = f x 1 st s f y f x 2 nd r y = f x 2 nd s f y f U = V x X y X f x G y = f x J f y f x H y = f x K f y
42 19 41 rabeqbidv r = R s = S f ran 1 st s ran 1 st r | f GId 2 nd r = GId 2 nd s x ran 1 st r y ran 1 st r f x 1 st r y = f x 1 st s f y f x 2 nd r y = f x 2 nd s f y = f Y X | f U = V x X y X f x G y = f x J f y f x H y = f x K f y
43 df-rngohom RngHom = r RingOps , s RingOps f ran 1 st s ran 1 st r | f GId 2 nd r = GId 2 nd s x ran 1 st r y ran 1 st r f x 1 st r y = f x 1 st s f y f x 2 nd r y = f x 2 nd s f y
44 ovex Y X V
45 44 rabex f Y X | f U = V x X y X f x G y = f x J f y f x H y = f x K f y V
46 42 43 45 ovmpoa R RingOps S RingOps R RngHom S = f Y X | f U = V x X y X f x G y = f x J f y f x H y = f x K f y