Metamath Proof Explorer


Theorem isrngohom

Description: The predicate "is a ring homomorphism from R to S ". (Contributed by Jeff Madsen, 19-Jun-2010)

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 isrngohom R RingOps S RingOps F R RngHom S F : X 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

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 1 2 3 4 5 6 7 8 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
10 9 eleq2d R RingOps S RingOps F R RngHom S F 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
11 5 fvexi J V
12 11 rnex ran J V
13 7 12 eqeltri Y V
14 1 fvexi G V
15 14 rnex ran G V
16 3 15 eqeltri X V
17 13 16 elmap F Y X F : X Y
18 17 anbi1i 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 F : X 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
19 fveq1 f = F f U = F U
20 19 eqeq1d f = F f U = V F U = V
21 fveq1 f = F f x G y = F x G y
22 fveq1 f = F f x = F x
23 fveq1 f = F f y = F y
24 22 23 oveq12d f = F f x J f y = F x J F y
25 21 24 eqeq12d f = F f x G y = f x J f y F x G y = F x J F y
26 fveq1 f = F f x H y = F x H y
27 22 23 oveq12d f = F f x K f y = F x K F y
28 26 27 eqeq12d f = F f x H y = f x K f y F x H y = F x K F y
29 25 28 anbi12d f = F f x G y = f x J f y f x H y = f x K f y F x G y = F x J F y F x H y = F x K F y
30 29 2ralbidv f = F x X y X f x G y = f x J f y f x H y = f x K f y x X y X F x G y = F x J F y F x H y = F x K F y
31 20 30 anbi12d f = F 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 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
32 31 elrab F 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 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
33 3anass F : X 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 F : X 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
34 18 32 33 3bitr4i F 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 F : X 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
35 10 34 bitrdi R RingOps S RingOps F R RngHom S F : X 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