ring_crt_pair_surjective

forall (R : Sort succ u), forall (addR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (eI : R), forall (eJ : R), forall (modI_surj : forall (y : RI), @RingImagePred.{succ u,succ v} R RI modI y), forall (modJ_surj : forall (y : RJ), @RingImagePred.{succ u,succ w} R RJ modJ y), forall (pair_eta : forall (z : P), @Eq.{succ p} P (pair (fst z) (snd z)) z), forall (combine_left : forall (a : R), forall (b : R), @Eq.{succ v} RI (modI (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modI a)), forall (combine_right : forall (a : R), forall (b : R), @Eq.{succ w} RJ (modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modJ b)), forall (y : P), @RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y

theorem ring_crt_pair_surjective.{p,u,v,w} :
  forall (R : Sort succ u), forall (addR : forall (a : R), forall (b : R), R), forall (mulR : forall (a : R), forall (b : R), R), forall (RI : Sort succ v), forall (RJ : Sort succ w), forall (P : Sort succ p), forall (pair : forall (x : RI), forall (y : RJ), P), forall (fst : forall (z : P), RI), forall (snd : forall (z : P), RJ), forall (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), forall (eI : R), forall (eJ : R), forall (modI_surj : forall (y : RI), @RingImagePred.{succ u,succ v} R RI modI y), forall (modJ_surj : forall (y : RJ), @RingImagePred.{succ u,succ w} R RJ modJ y), forall (pair_eta : forall (z : P), @Eq.{succ p} P (pair (fst z) (snd z)) z), forall (combine_left : forall (a : R), forall (b : R), @Eq.{succ v} RI (modI (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modI a)), forall (combine_right : forall (a : R), forall (b : R), @Eq.{succ w} RJ (modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modJ b)), forall (y : P), @RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y :=
  fun R => fun addR => fun mulR => fun RI => fun RJ => fun P => fun pair => fun fst => fun snd => fun modI => fun modJ => fun eI => fun eJ => fun modI_surj => fun modJ_surj => fun pair_eta => fun combine_left => fun combine_right => fun y => modI_surj (fst y) (@RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y) (fun (a : R) => fun (ha : @Eq.{succ v} RI (modI a) (fst y)) => modJ_surj (snd y) (@RingImagePred.{succ u,succ p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y) (fun (b : R) => fun (hb : @Eq.{succ w} RJ (modJ b) (snd y)) => fun (Q : Prop) => fun (mk : forall (x : R), forall (h : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) y), Q) => mk (@RingCrtCombine.{succ u} R addR mulR eI eJ a b) (@eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (pair (modI a) (modJ b)) y (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modI a) (modJ (@RingCrtCombine.{succ u} R addR mulR eI eJ a b)) (modJ b) (combine_left a b) (combine_right a b)) (@eq_trans.{succ p} P (pair (modI a) (modJ b)) (pair (fst y) (snd y)) y (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI a) (fst y) (modJ b) (snd y) ha hb) (pair_eta y)))))