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