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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
rnghomval.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
rnghomval.3 ⊢ 𝑋 = ran 𝐺
rnghomval.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
rnghomval.5 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
rnghomval.6 ⊢ 𝐾 = ( 2nd ‘ 𝑆 )
rnghomval.7 ⊢ 𝑌 = ran 𝐽
rnghomval.8 ⊢ 𝑉 = ( GId ‘ 𝐾 )
Assertion isrngohom ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rnghomval.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 rnghomval.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 rnghomval.3 ⊢ 𝑋 = ran 𝐺
4 rnghomval.4 ⊢ 𝑈 = ( GId ‘ 𝐻 )
5 rnghomval.5 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
6 rnghomval.6 ⊢ 𝐾 = ( 2nd ‘ 𝑆 )
7 rnghomval.7 ⊢ 𝑌 = ran 𝐽
8 rnghomval.8 ⊢ 𝑉 = ( GId ‘ 𝐾 )
9 1 2 3 4 5 6 7 8 rngohomval ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RngHom 𝑆 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } )
10 9 eleq2d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } ) )
11 5 fvexi ⊢ 𝐽 ∈ V
12 11 rnex ⊢ ran 𝐽 ∈ V
13 7 12 eqeltri ⊢ 𝑌 ∈ V
14 1 fvexi ⊢ 𝐺 ∈ V
15 14 rnex ⊢ ran 𝐺 ∈ V
16 3 15 eqeltri ⊢ 𝑋 ∈ V
17 13 16 elmap ⊢ ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ 𝑌 )
18 17 anbi1i ⊢ ( ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
19 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑈 ) )
20 19 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ↔ ( 𝐹 ‘ 𝑈 ) = 𝑉 ) )
21 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) )
22 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
23 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
24 22 23 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
25 21 24 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
26 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) )
27 22 23 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) )
28 26 27 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) )
29 25 28 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) )
30 29 2ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) )
31 20 30 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
32 31 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } ↔ ( 𝐹 ∈ ( 𝑌 ↑m 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
33 3anass ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
34 18 32 33 3bitr4i ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ( ( 𝑓 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑓 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝐾 ( 𝑓 ‘ 𝑦 ) ) ) ) } ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) )
35 10 34 bitrdi ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ 𝑈 ) = 𝑉 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐾 ( 𝐹 ‘ 𝑦 ) ) ) ) ) )