ring_image_add_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 (addS x y)

theorem ring_image_add_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 (addS 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 (addS x y)) (fun (a : R) => fun (hax : @Eq.{v} S (f a) x) => hy (@RingImagePred.{u,v} R S f (addS 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) (addS x y)), P) => mk (addR a b) (@eq_trans.{v} S (f (addR a b)) (addS (f a) (f b)) (addS x y) (@ring_hom_add.{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 addS (f a) x (f b) y hax hby))))