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 36842
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 2733 . . . . . . 7 (1st β€˜π‘†) = (1st β€˜π‘†)
2 eqid 2733 . . . . . . 7 ran (1st β€˜π‘†) = ran (1st β€˜π‘†)
3 eqid 2733 . . . . . . 7 (1st β€˜π‘‡) = (1st β€˜π‘‡)
4 eqid 2733 . . . . . . 7 ran (1st β€˜π‘‡) = ran (1st β€˜π‘‡)
51, 2, 3, 4rngohomf 36834 . . . . . 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 2733 . . . . . . 7 (1st β€˜π‘…) = (1st β€˜π‘…)
10 eqid 2733 . . . . . . 7 ran (1st β€˜π‘…) = ran (1st β€˜π‘…)
119, 10, 1, 2rngohomf 36834 . . . . . 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 6742 . . 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 2733 . . . . . . 7 (2nd β€˜π‘…) = (2nd β€˜π‘…)
18 eqid 2733 . . . . . . 7 (GIdβ€˜(2nd β€˜π‘…)) = (GIdβ€˜(2nd β€˜π‘…))
1910, 17, 18rngo1cl 36807 . . . . . 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 6991 . . . 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 2733 . . . . . . . . 9 (2nd β€˜π‘†) = (2nd β€˜π‘†)
25 eqid 2733 . . . . . . . . 9 (GIdβ€˜(2nd β€˜π‘†)) = (GIdβ€˜(2nd β€˜π‘†))
2617, 18, 24, 25rngohom1 36836 . . . . . . . 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 6896 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))) = (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))))
31 eqid 2733 . . . . . . . 8 (2nd β€˜π‘‡) = (2nd β€˜π‘‡)
32 eqid 2733 . . . . . . . 8 (GIdβ€˜(2nd β€˜π‘‡)) = (GIdβ€˜(2nd β€˜π‘‡))
3324, 25, 31, 32rngohom1 36836 . . . . . . 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 2773 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))) = (GIdβ€˜(2nd β€˜π‘‡)))
3823, 37eqtrd 2773 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)))
399, 10, 1rngohomadd 36837 . . . . . . . . . . . 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 6896 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))) = (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
469, 10, 1, 2rngohomcl 36835 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†))
479, 10, 1, 2rngohomcl 36835 . . . . . . . . . . . . 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 36837 . . . . . . . . . . . 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 2773 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
629, 10rngogcl 36780 . . . . . . . . 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 6991 . . . . . . 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 6991 . . . . . . . 8 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)))
7014, 69sylan 581 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)))
71 fvco3 6991 . . . . . . . 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 7418 . . . . . 6 ((((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
7573, 74syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
7661, 68, 753eqtr4d 2783 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)))
779, 10, 17, 24rngohommul 36838 . . . . . . . . . . . 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 6896 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))) = (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
841, 2, 24, 31rngohommul 36838 . . . . . . . . . . . 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 2773 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
929, 17, 10rngocl 36769 . . . . . . . . 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 6991 . . . . . . 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 7418 . . . . . 6 ((((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
10073, 99syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
10191, 98, 1003eqtr4d 2783 . . . 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 3201 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐺 ∈ (𝑆 RngHom 𝑇))) β†’ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))
1049, 17, 10, 18, 3, 31, 4, 32isrngohom 36833 . . . 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 3062  ran crn 5678   ∘ ccom 5681  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  1st c1st 7973  2nd c2nd 7974  GIdcgi 29743  RingOpscrngo 36762   RngHom crnghom 36828
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 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fo 6550  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-map 8822  df-grpo 29746  df-gid 29747  df-ablo 29798  df-ass 36711  df-exid 36713  df-mgmOLD 36717  df-sgrOLD 36729  df-mndo 36735  df-rngo 36763  df-rngohom 36831
This theorem is referenced by:  rngoisoco  36850
  Copyright terms: Public domain W3C validator