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 𝑆 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ( 𝐹𝑈 ) = 𝑉 ∧ ∀ 𝑥𝑋𝑦𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹𝑥 ) 𝐽 ( 𝐹𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 𝐻 𝑦 ) ) = ( ( 𝐹𝑥 ) 𝐾 ( 𝐹𝑦 ) ) ) ) ) )