ring_image_mul_closed

forall (R : Sort u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (S : Sort v), forall (zeroS : S), forall (oneS : S), forall (addS : forall (a : S), forall (b : S), S), forall (negS : forall (a : S), S), forall (subS : forall (a : S), forall (b : S), S), forall (mulS : forall (a : S), forall (b : S), S), forall (f : forall (x : R), S), forall (hom_args : @RingHomLawArgs.{u,v} R zeroR oneR addR negR subR mulR S zeroS oneS addS negS subS mulS f), forall (x : S), forall (y : S), forall (hx : @RingImagePred.{u,v} R S f x), forall (hy : @RingImagePred.{u,v} R S f y), @RingImagePred.{u,v} R S f (mulS x y)

theorem ring_image_mul_closed.{u,v} :
  forall (R : Sort u), forall (zeroR : R), forall (oneR : R), forall (addR : forall (a : R), forall (b : R), R), forall (negR : forall (a : R), R), forall (subR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (S : Sort v), forall (zeroS : S), forall (oneS : S), forall (addS : forall (a : S), forall (b : S), S), forall (negS : forall (a : S), S), forall (subS : forall (a : S), forall (b : S), S), forall (mulS : forall (a : S), forall (b : S), S), forall (f : forall (x : R), S), forall (hom_args : @RingHomLawArgs.{u,v} R zeroR oneR addR negR subR mulR S zeroS oneS addS negS subS mulS f), forall (x : S), forall (y : S), forall (hx : @RingImagePred.{u,v} R S f x), forall (hy : @RingImagePred.{u,v} R S f y), @RingImagePred.{u,v} R S f (mulS x y) :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun S => fun zeroS => fun oneS => fun addS => fun negS => fun subS => fun mulS => fun f => fun hom_args => fun x => fun y => fun hx => fun hy => hx (@RingImagePred.{u,v} R S f (mulS x y)) (fun (a : R) => fun (hax : @Eq.{v} S (f a) x) => hy (@RingImagePred.{u,v} R S f (mulS x y)) (fun (b : R) => fun (hby : @Eq.{v} S (f b) y) => fun (P : Prop) => fun (mk : forall (c : R), forall (h : @Eq.{v} S (f c) (mulS x y)), P) => mk (mulR a b) (@eq_trans.{v} S (f (mulR a b)) (mulS (f a) (f b)) (mulS x y) (@ring_hom_mul.{u,v} R zeroR oneR addR negR subR mulR S zeroS oneS addS negS subS mulS f hom_args a b) (@eq_congr2.{v,v,v} S S S mulS (f a) x (f b) y hax hby))))