ring_crt_pair_hom_laws

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 (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), 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))), @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)

theorem ring_crt_pair_hom_laws.{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 (modI : forall (x : R), RI), forall (modJ : forall (x : R), RJ), 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))), @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) :=
  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 modI => fun modJ => fun homI_args => fun homJ_args => fun zero_pair => fun one_pair => fun add_pair => fun neg_pair => fun mul_pair => fun (Q : Prop) => fun (mk : forall (hom_zero_law : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ zeroR) zeroP), forall (hom_one_law : @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ oneR) oneP), forall (hom_add_law : forall (a : R), forall (b : R), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (addR a b)) (addP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b))), forall (hom_neg_law : forall (a : R), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (negR a)) (negP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a))), forall (hom_mul_law : forall (a : R), forall (b : R), @Eq.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (mulR a b)) (mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b))), Q) => mk (@eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ zeroR) (pair zeroI zeroJ) zeroP (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI zeroR) zeroI (modJ zeroR) zeroJ (@ring_hom_zero.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args) (@ring_hom_zero.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args)) zero_pair) (@eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ oneR) (pair oneI oneJ) oneP (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI oneR) oneI (modJ oneR) oneJ (@ring_hom_one.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args) (@ring_hom_one.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args)) one_pair) (fun (a : R) => fun (b : R) => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (addR a b)) (pair (addI (modI a) (modI b)) (addJ (modJ a) (modJ b))) (addP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b)) (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (addR a b)) (addI (modI a) (modI b)) (modJ (addR a b)) (addJ (modJ a) (modJ b)) (@ring_hom_add.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args a b) (@ring_hom_add.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args a b)) (add_pair (modI a) (modI b) (modJ a) (modJ b))) (fun (a : R) => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (negR a)) (pair (negI (modI a)) (negJ (modJ a))) (negP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a)) (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (negR a)) (negI (modI a)) (modJ (negR a)) (negJ (modJ a)) (@ring_hom_neg.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args a) (@ring_hom_neg.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args a)) (neg_pair (modI a) (modJ a))) (fun (a : R) => fun (b : R) => @eq_trans.{succ p} P (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ (mulR a b)) (pair (mulI (modI a) (modI b)) (mulJ (modJ a) (modJ b))) (mulP (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ a) (@RingCrtPairMap.{succ p,succ u,succ v,succ w} R RI RJ P pair modI modJ b)) (@eq_congr2.{succ v,succ w,succ p} RI RJ P pair (modI (mulR a b)) (mulI (modI a) (modI b)) (modJ (mulR a b)) (mulJ (modJ a) (modJ b)) (@ring_hom_mul.{succ u,succ v} R zeroR oneR addR negR subR mulR RI zeroI oneI addI negI subI mulI modI homI_args a b) (@ring_hom_mul.{succ u,succ w} R zeroR oneR addR negR subR mulR RJ zeroJ oneJ addJ negJ subJ mulJ modJ homJ_args a b)) (mul_pair (modI a) (modI b) (modJ a) (modJ b)))