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 37145
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) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇))

Proof of Theorem rngohomco
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2730 . . . . . . 7 (1st β€˜π‘†) = (1st β€˜π‘†)
2 eqid 2730 . . . . . . 7 ran (1st β€˜π‘†) = ran (1st β€˜π‘†)
3 eqid 2730 . . . . . . 7 (1st β€˜π‘‡) = (1st β€˜π‘‡)
4 eqid 2730 . . . . . . 7 ran (1st β€˜π‘‡) = ran (1st β€˜π‘‡)
51, 2, 3, 4rngohomf 37137 . . . . . 6 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
653expa 1116 . . . . 5 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
763adantl1 1164 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
87adantrl 712 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ 𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡))
9 eqid 2730 . . . . . . 7 (1st β€˜π‘…) = (1st β€˜π‘…)
10 eqid 2730 . . . . . . 7 ran (1st β€˜π‘…) = ran (1st β€˜π‘…)
119, 10, 1, 2rngohomf 37137 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
12113expa 1116 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
13123adantl3 1166 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
1413adantrr 713 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†))
15 fco 6740 . . 3 ((𝐺:ran (1st β€˜π‘†)⟢ran (1st β€˜π‘‡) ∧ 𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†)) β†’ (𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡))
168, 14, 15syl2anc 582 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡))
17 eqid 2730 . . . . . . 7 (2nd β€˜π‘…) = (2nd β€˜π‘…)
18 eqid 2730 . . . . . . 7 (GIdβ€˜(2nd β€˜π‘…)) = (GIdβ€˜(2nd β€˜π‘…))
1910, 17, 18rngo1cl 37110 . . . . . 6 (𝑅 ∈ RingOps β†’ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…))
20193ad2ant1 1131 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) β†’ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…))
2120adantr 479 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…))
22 fvco3 6989 . . . 4 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ (GIdβ€˜(2nd β€˜π‘…)) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))))
2314, 21, 22syl2anc 582 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))))
24 eqid 2730 . . . . . . . . 9 (2nd β€˜π‘†) = (2nd β€˜π‘†)
25 eqid 2730 . . . . . . . . 9 (GIdβ€˜(2nd β€˜π‘†)) = (GIdβ€˜(2nd β€˜π‘†))
2617, 18, 24, 25rngohom1 37139 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
27263expa 1116 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
28273adantl3 1166 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
2928adantrr 713 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (πΉβ€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘†)))
3029fveq2d 6894 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))) = (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))))
31 eqid 2730 . . . . . . . 8 (2nd β€˜π‘‡) = (2nd β€˜π‘‡)
32 eqid 2730 . . . . . . . 8 (GIdβ€˜(2nd β€˜π‘‡)) = (GIdβ€˜(2nd β€˜π‘‡))
3324, 25, 31, 32rngohom1 37139 . . . . . . 7 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
34333expa 1116 . . . . . 6 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
35343adantl1 1164 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
3635adantrl 712 . . . 4 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (πΊβ€˜(GIdβ€˜(2nd β€˜π‘†))) = (GIdβ€˜(2nd β€˜π‘‡)))
3730, 36eqtrd 2770 . . 3 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (πΊβ€˜(πΉβ€˜(GIdβ€˜(2nd β€˜π‘…)))) = (GIdβ€˜(2nd β€˜π‘‡)))
3823, 37eqtrd 2770 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)))
399, 10, 1rngohomadd 37140 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦)))
4039ex 411 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
41403expa 1116 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
42413adantl3 1166 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
4342imp 405 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦)))
4443adantlrr 717 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦)))
4544fveq2d 6894 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))) = (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))))
469, 10, 1, 2rngohomcl 37138 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†))
479, 10, 1, 2rngohomcl 37138 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))
4846, 47anim12dan 617 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)))
4948ex 411 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))))
50493expa 1116 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))))
51503adantl3 1166 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))))
5251imp 405 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)))
5352adantlrr 717 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)))
541, 2, 3rngohomadd 37140 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
5554ex 411 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
56553expa 1116 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
57563adantl1 1164 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
5857imp 405 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
5958adantlrl 716 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
6053, 59syldan 589 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(1st β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
6145, 60eqtrd 2770 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
629, 10rngogcl 37083 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
63623expb 1118 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
64633ad2antl1 1183 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
6564adantlr 711 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
66 fvco3 6989 . . . . . . 7 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))))
6714, 66sylan 578 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯(1st β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))))
6865, 67syldan 589 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(1st β€˜π‘…)𝑦))))
69 fvco3 6989 . . . . . . . 8 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)))
7014, 69sylan 578 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ π‘₯ ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)))
71 fvco3 6989 . . . . . . . 8 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦)))
7214, 71sylan 578 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦)))
7370, 72anim12dan 617 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))))
74 oveq12 7420 . . . . . 6 ((((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
7573, 74syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(1st β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
7661, 68, 753eqtr4d 2780 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)))
779, 10, 17, 24rngohommul 37141 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦)))
7877ex 411 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
79783expa 1116 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
80793adantl3 1166 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) β†’ ((π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
8180imp 405 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦)))
8281adantlrr 717 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦)))
8382fveq2d 6894 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))) = (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))))
841, 2, 24, 31rngohommul 37141 . . . . . . . . . . . 12 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
8584ex 411 . . . . . . . . . . 11 ((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
86853expa 1116 . . . . . . . . . 10 (((𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
87863adantl1 1164 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) β†’ (((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†)) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦)))))
8887imp 405 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇)) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
8988adantlrl 716 . . . . . . 7 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ ((πΉβ€˜π‘₯) ∈ ran (1st β€˜π‘†) ∧ (πΉβ€˜π‘¦) ∈ ran (1st β€˜π‘†))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
9053, 89syldan 589 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜((πΉβ€˜π‘₯)(2nd β€˜π‘†)(πΉβ€˜π‘¦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
9183, 90eqtrd 2770 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
929, 17, 10rngocl 37072 . . . . . . . . 9 ((𝑅 ∈ RingOps ∧ π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…)) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
93923expb 1118 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
94933ad2antl1 1183 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
9594adantlr 711 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…))
96 fvco3 6989 . . . . . . 7 ((𝐹:ran (1st β€˜π‘…)⟢ran (1st β€˜π‘†) ∧ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))))
9714, 96sylan 578 . . . . . 6 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯(2nd β€˜π‘…)𝑦) ∈ ran (1st β€˜π‘…)) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))))
9895, 97syldan 589 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (πΊβ€˜(πΉβ€˜(π‘₯(2nd β€˜π‘…)𝑦))))
99 oveq12 7420 . . . . . 6 ((((𝐺 ∘ 𝐹)β€˜π‘₯) = (πΊβ€˜(πΉβ€˜π‘₯)) ∧ ((𝐺 ∘ 𝐹)β€˜π‘¦) = (πΊβ€˜(πΉβ€˜π‘¦))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
10073, 99syl 17 . . . . 5 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) = ((πΊβ€˜(πΉβ€˜π‘₯))(2nd β€˜π‘‡)(πΊβ€˜(πΉβ€˜π‘¦))))
10191, 98, 1003eqtr4d 2780 . . . 4 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)))
10276, 101jca 510 . . 3 ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) ∧ (π‘₯ ∈ ran (1st β€˜π‘…) ∧ 𝑦 ∈ ran (1st β€˜π‘…))) β†’ (((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))
103102ralrimivva 3198 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))
1049, 17, 10, 18, 3, 31, 4, 32isrngohom 37136 . . . 4 ((𝑅 ∈ RingOps ∧ 𝑇 ∈ RingOps) β†’ ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡) ∧ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)) ∧ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))))
1051043adant2 1129 . . 3 ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) β†’ ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡) ∧ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)) ∧ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))))
106105adantr 479 . 2 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ ((𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇) ↔ ((𝐺 ∘ 𝐹):ran (1st β€˜π‘…)⟢ran (1st β€˜π‘‡) ∧ ((𝐺 ∘ 𝐹)β€˜(GIdβ€˜(2nd β€˜π‘…))) = (GIdβ€˜(2nd β€˜π‘‡)) ∧ βˆ€π‘₯ ∈ ran (1st β€˜π‘…)βˆ€π‘¦ ∈ ran (1st β€˜π‘…)(((𝐺 ∘ 𝐹)β€˜(π‘₯(1st β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(1st β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦)) ∧ ((𝐺 ∘ 𝐹)β€˜(π‘₯(2nd β€˜π‘…)𝑦)) = (((𝐺 ∘ 𝐹)β€˜π‘₯)(2nd β€˜π‘‡)((𝐺 ∘ 𝐹)β€˜π‘¦))))))
10716, 38, 103, 106mpbir3and 1340 1 (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝑇 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RingOpsHom 𝑆) ∧ 𝐺 ∈ (𝑆 RingOpsHom 𝑇))) β†’ (𝐺 ∘ 𝐹) ∈ (𝑅 RingOpsHom 𝑇))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  ran crn 5676   ∘ ccom 5679  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976  GIdcgi 30010  RingOpscrngo 37065   RingOpsHom crngohom 37131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fo 6548  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-map 8824  df-grpo 30013  df-gid 30014  df-ablo 30065  df-ass 37014  df-exid 37016  df-mgmOLD 37020  df-sgrOLD 37032  df-mndo 37038  df-rngo 37066  df-rngohom 37134
This theorem is referenced by:  rngoisoco  37153
  Copyright terms: Public domain W3C validator