Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rngohomco Structured version   Visualization version   GIF version

Theorem rngohomco 36436
Description: The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.)
Assertion
Ref Expression
rngohomco (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (𝐺 ∘ 𝐹) ∈ (𝑅 RngHom 𝑇))

Proof of Theorem rngohomco
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . . . . . 7 (1st β€˜π‘†) = (1st β€˜π‘†)
2 eqid 2737 . . . . . . 7 ran (1st β€˜π‘†) = ran (1st β€˜π‘†)
3 eqid 2737 . . . . . . 7 (1st β€˜π‘‡) = (1st β€˜π‘‡)
4 eqid 2737 . . . . . . 7 ran (1st β€˜π‘‡) = ran (1st β€˜π‘‡)
51, 2, 3, 4rngohomf 36428 . . . . . 6 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
653expa 1119 . . . . 5 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
763adantl1 1167 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
87adantrl 715 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
9 eqid 2737 . . . . . . 7 (1st β€˜π‘…) = (1st β€˜π‘…)
10 eqid 2737 . . . . . . 7 ran (1st β€˜π‘…) = ran (1st β€˜π‘…)
119, 10, 1, 2rngohomf 36428 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
12113expa 1119 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
13123adantl3 1169 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
1413adantrr 716 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
15 fco 6693 . . 3 ((𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡) ∧ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†)) β†’ (𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡))
168, 14, 15syl2anc 585 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡))
17 eqid 2737 . . . . . . 7 (2nd β€˜π‘…) = (2nd β€˜π‘…)
18 eqid 2737 . . . . . . 7 (GIdβ€˜(2nd β€˜π‘…)) = (GIdβ€˜(2nd β€˜π‘…))
1910, 17, 18rngo1cl 36401 . . . . . 6 (𝑅 ∈ RingOps β†’ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…))
20193ad2ant1 1134 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) β†’ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…))
2120adantr 482 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…))
22 fvco3 6941 . . . 4 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))))
2314, 21, 22syl2anc 585 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))))
24 eqid 2737 . . . . . . . . 9 (2nd β€˜π‘†) = (2nd β€˜π‘†)
25 eqid 2737 . . . . . . . . 9 (GIdβ€˜(2nd β€˜π‘†)) = (GIdβ€˜(2nd β€˜π‘†))
2617, 18, 24, 25rngohom1 36430 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
27263expa 1119 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
28273adantl3 1169 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
2928adantrr 716 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
3029fveq2d 6847 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))) = (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))))
31 eqid 2737 . . . . . . . 8 (2nd β€˜π‘‡) = (2nd β€˜π‘‡)
32 eqid 2737 . . . . . . . 8 (GIdβ€˜(2nd β€˜π‘‡)) = (GIdβ€˜(2nd β€˜π‘‡))
3324, 25, 31, 32rngohom1 36430 . . . . . . 7 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
34333expa 1119 . . . . . 6 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
35343adantl1 1167 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
3635adantrl 715 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
3730, 36eqtrd 2777 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))) = (GIdβ€˜(2nd β€˜π‘‡)))
3823, 37eqtrd 2777 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)))
399, 10, 1rngohomadd 36431 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦)))
4039ex 414 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
41403expa 1119 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
42413adantl3 1169 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
4342imp 408 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦)))
4443adantlrr 720 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦)))
4544fveq2d 6847 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))) = (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
469, 10, 1, 2rngohomcl 36429 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†))
479, 10, 1, 2rngohomcl 36429 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))
4846, 47anim12dan 620 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)))
4948ex 414 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))))
50493expa 1119 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))))
51503adantl3 1169 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))))
5251imp 408 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)))
5352adantlrr 720 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)))
541, 2, 3rngohomadd 36431 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
5554ex 414 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
56553expa 1119 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
57563adantl1 1167 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
5857imp 408 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
5958adantlrl 719 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
6053, 59syldan 592 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
6145, 60eqtrd 2777 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
629, 10rngogcl 36374 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
63623expb 1121 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
64633ad2antl1 1186 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
6564adantlr 714 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
66 fvco3 6941 . . . . . . 7 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))))
6714, 66sylan 581 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))))
6865, 67syldan 592 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))))
69 fvco3 6941 . . . . . . . 8 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)))
7014, 69sylan 581 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)))
71 fvco3 6941 . . . . . . . 8 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦)))
7214, 71sylan 581 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦)))
7370, 72anim12dan 620 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))))
74 oveq12 7367 . . . . . 6 ((((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
7573, 74syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
7661, 68, 753eqtr4d 2787 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)))
779, 10, 17, 24rngohommul 36432 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦)))
7877ex 414 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
79783expa 1119 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
80793adantl3 1169 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
8180imp 408 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦)))
8281adantlrr 720 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦)))
8382fveq2d 6847 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))) = (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
841, 2, 24, 31rngohommul 36432 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
8584ex 414 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
86853expa 1119 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
87863adantl1 1167 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
8887imp 408 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
8988adantlrl 719 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
9053, 89syldan 592 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
9183, 90eqtrd 2777 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
929, 17, 10rngocl 36363 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
93923expb 1121 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
94933ad2antl1 1186 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
9594adantlr 714 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
96 fvco3 6941 . . . . . . 7 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))))
9714, 96sylan 581 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))))
9895, 97syldan 592 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))))
99 oveq12 7367 . . . . . 6 ((((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
10073, 99syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
10191, 98, 1003eqtr4d 2787 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)))
10276, 101jca 513 . . 3 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))
103102ralrimivva 3198 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))
1049, 17, 10, 18, 3, 31, 4, 32isrngohom 36427 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps) β†’ ((𝐺 ∘ 𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡) ∧ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)) ∧ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))))
1051043adant2 1132 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) β†’ ((𝐺 ∘ 𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡) ∧ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)) ∧ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))))
106105adantr 482 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ ((𝐺 ∘ 𝐹) ∈ (𝑅 RngHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡) ∧ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)) ∧ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))))
10716, 38, 103, 106mpbir3and 1343 1 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (𝐺 ∘ 𝐹) ∈ (𝑅 RngHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3065  ran crn 5635   ∘ ccom 5638  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  1st c1st 7920  2nd c2nd 7921  GIdcgi 29435  RingOpscrngo 36356   RngHom crnghom 36422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fo 6503  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-map 8768  df-grpo 29438  df-gid 29439  df-ablo 29490  df-ass 36305  df-exid 36307  df-mgmOLD 36311  df-sgrOLD 36323  df-mndo 36329  df-rngo 36357  df-rngohom 36425
This theorem is referenced by:  rngoisoco  36444
  Copyright terms: Public domain W3C validator