ring_chinese_remainder_theorem

forall (R : Sort succ 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 (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), 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 (ringR_args : @RingLawArgs.{succ u} R zeroR oneR addR negR subR mulR), forall (ringP_args : @RingLawArgs.{succ p} P zeroP oneP addP negP subP mulP), forall (homI_args : @RingHomLawArgs.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI), forall (homJ_args : @RingHomLawArgs.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (one_pair : @Eq.{succ p} P (pair oneI oneJ) oneP), forall (add_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (addI xI yI) (addJ xJ yJ)) (addP (pair xI xJ) (pair yI yJ))), forall (neg_pair : forall (xI : RI), forall (xJ : RJ), @Eq.{succ p} P (pair (negI xI) (negJ xJ)) (negP (pair xI xJ))), forall (mul_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (mulI xI yI) (mulJ xJ yJ)) (mulP (pair xI xJ) (pair yI yJ))), forall (fst_pair : forall (x : RI), forall (y : RJ), @Eq.{succ v} RI (fst (pair x y)) x), forall (snd_pair : forall (x : RI), forall (y : RJ), @Eq.{succ w} RJ (snd (pair x y)) y), forall (pair_eta : forall (z : P), @Eq.{succ p} P (pair (fst z) (snd z)) z), 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 (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)), @RingChineseRemainder.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair fst snd modI modJ ringR_args ringP_args

theorem ring_chinese_remainder_theorem.{p,u,v,w} :
  forall (R : Sort succ 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 (RI : Sort succ v), forall (zeroI : RI), forall (oneI : RI), forall (addI : forall (a : RI), forall (b : RI), RI), forall (negI : forall (a : RI), RI), forall (subI : forall (a : RI), forall (b : RI), RI), forall (mulI : forall (a : RI), forall (b : RI), RI), forall (RJ : Sort succ w), forall (zeroJ : RJ), forall (oneJ : RJ), forall (addJ : forall (a : RJ), forall (b : RJ), RJ), forall (negJ : forall (a : RJ), RJ), forall (subJ : forall (a : RJ), forall (b : RJ), RJ), forall (mulJ : forall (a : RJ), forall (b : RJ), RJ), forall (P : Sort succ p), forall (zeroP : P), forall (oneP : P), forall (addP : forall (a : P), forall (b : P), P), forall (negP : forall (a : P), P), forall (subP : forall (a : P), forall (b : P), P), forall (mulP : forall (a : P), forall (b : P), 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 (ringR_args : @RingLawArgs.{succ u} R zeroR oneR addR negR subR mulR), forall (ringP_args : @RingLawArgs.{succ p} P zeroP oneP addP negP subP mulP), forall (homI_args : @RingHomLawArgs.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI), forall (homJ_args : @RingHomLawArgs.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ), forall (zero_pair : @Eq.{succ p} P (pair zeroI zeroJ) zeroP), forall (one_pair : @Eq.{succ p} P (pair oneI oneJ) oneP), forall (add_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (addI xI yI) (addJ xJ yJ)) (addP (pair xI xJ) (pair yI yJ))), forall (neg_pair : forall (xI : RI), forall (xJ : RJ), @Eq.{succ p} P (pair (negI xI) (negJ xJ)) (negP (pair xI xJ))), forall (mul_pair : forall (xI : RI), forall (yI : RI), forall (xJ : RJ), forall (yJ : RJ), @Eq.{succ p} P (pair (mulI xI yI) (mulJ xJ yJ)) (mulP (pair xI xJ) (pair yI yJ))), forall (fst_pair : forall (x : RI), forall (y : RJ), @Eq.{succ v} RI (fst (pair x y)) x), forall (snd_pair : forall (x : RI), forall (y : RJ), @Eq.{succ w} RJ (snd (pair x y)) y), forall (pair_eta : forall (z : P), @Eq.{succ p} P (pair (fst z) (snd z)) z), 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 (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)), @RingChineseRemainder.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair fst snd modI modJ ringR_args ringP_args :=
  fun R => fun zeroR => fun oneR => fun addR => fun negR => fun subR => fun mulR => fun RI => fun zeroI => fun oneI => fun addI => fun negI => fun subI => fun mulI => fun RJ => fun zeroJ => fun oneJ => fun addJ => fun negJ => fun subJ => fun mulJ => fun P => fun zeroP => fun oneP => fun addP => fun negP => fun subP => fun mulP => fun pair => fun fst => fun snd => fun modI => fun modJ => fun eI => fun eJ => fun ringR_args => fun ringP_args => fun homI_args => fun homJ_args => fun zero_pair => fun one_pair => fun add_pair => fun neg_pair => fun mul_pair => fun fst_pair => fun snd_pair => fun pair_eta => fun modI_surj => fun modJ_surj => fun combine_left => fun combine_right => fun (Q : Prop) => fun (mk : forall (pair_hom : @RingHomLawArgs.{succ u,succ p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (kernel_to_intersection : 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) zeroP), @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), forall (intersection_to_kernel : forall (x : R), forall (h : @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP), forall (first_iso_to_image : @RingFirstIso.{u,p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) ringR_args ringP_args pair_hom), forall (full_product_image : 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), forall (quot_surj_product : forall (y : P), forall (S : Prop), forall (mk_surj : forall (q : @RingKerQuot.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (h : @Eq.{succ p} P (@RingKerQuotToS.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) q) y), S), S), Q) => mk (@ring_crt_pair_hom_laws.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair modI modJ homI_args homJ_args zero_pair one_pair add_pair neg_pair mul_pair) (@ring_crt_kernel_to_intersection.{p,u,v,w} R RI RJ P zeroI zeroJ zeroP pair fst snd modI modJ fst_pair snd_pair zero_pair) (fun (x : R) => fun (h : @RingCrtIntersectionPred.{succ u,succ v,succ w} R RI RJ zeroI zeroJ modI modJ x) => h (@Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ x) zeroP) (fun (left_kernel : @Eq.{succ v} RI (modI x) zeroI) => fun (right_kernel : @Eq.{succ w} RJ (modJ x) zeroJ) => @ring_crt_intersection_to_kernel.{p,u,v,w} R RI RJ P zeroI zeroJ zeroP pair modI modJ zero_pair x left_kernel right_kernel)) (@ring_first_isomorphism_to_image.{u,p} R zeroR oneR addR negR subR mulR P zeroP oneP addP negP subP mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) ringR_args ringP_args (@ring_crt_pair_hom_laws.{p,u,v,w} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI RJ zeroJ oneJ addJ negJ subJ mulJ P zeroP oneP addP negP subP mulP pair modI modJ homI_args homJ_args zero_pair one_pair add_pair neg_pair mul_pair)) (@ring_crt_pair_surjective.{p,u,v,w} R addR mulR RI RJ P pair fst snd modI modJ eI eJ modI_surj modJ_surj pair_eta combine_left combine_right) (fun (y : P) => fun (S : Prop) => fun (mk_surj : forall (q : @RingKerQuot.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ)), forall (h : @Eq.{succ p} P (@RingKerQuotToS.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) q) y), S) => @ring_first_iso_phi_surj_image.{u,p} R P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ) y (@ring_crt_pair_surjective.{p,u,v,w} R addR mulR RI RJ P pair fst snd modI modJ eI eJ modI_surj modJ_surj pair_eta combine_left combine_right y) S mk_surj)