proposition: Lemma isringfunweqfldfracgt_b (X : intdom) (is : isdeceq X) {R : hrel X} (is1 : isringmultgt X R) (is2 : R 1 0) (ir : isirrefl R) : isringfun (weqfldfracgt_b X is is1 is2 ir).
proof: Proof. intros. set (g := weqfldfracgt_b X is is1 is2 ir). set (g0 := weqfldfracgtint_b X is1 is2 ir). split. - split. + unfold isbinopfun. change (∏ x x' : commringfrac X (ringpossubmonoid X is1 is2), paths (g (x + x')) ((g x) + (g x'))). apply (setquotuniv2prop _ (λ x x' : commringfrac X (ringpossubmonoid X is1 is2), make_hProp _ (setproperty (fldfrac X is) (g (x + x')) ((g x) + (g x'))))). intros xa1 xa2. change (paths (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (g0 (commringfracop1int X (ringpossubmonoid X is1 is2) xa1 xa2))) (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (commringfracop1int X (intdomnonzerosubmonoid X) (g0 xa1) (g0 xa2)))). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. unfold commringfracop1int. simpl. apply (pathsdirprod). * apply idpath. * destruct xa1 as [ x1 aa1 ]. destruct xa2 as [ x2 aa2 ]. simpl. destruct aa1 as [ a1 ia1 ]. destruct aa2 as [ a2 ia2 ]. simpl. apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (tpair _ (a1 * a2) (rtoneq ir (is1 a1 a2 ia1 ia2))) (make_carrier (λ x : pr1 X, make_hProp (x = 0 -> empty) (isapropneg (x = 0))) (a1 * a2) (fun e : paths (a1 * a2) 0 => toneghdisj (make_dirprod (rtoneq ir ia1) (rtoneq ir ia2)) (intdomax X a1 a2 e))) (idpath _)). + change (paths (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (g0 (make_dirprod 0 (tpair _ 1 is2)))) (setquotpr _ (make_dirprod 0 (tpair _ 1 (nonzeroax X))))). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. simpl. apply pathsdirprod. * apply idpath. * apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (tpair _ 1 (rtoneq ir is2)) (tpair _ 1 (nonzeroax X))). simpl. apply idpath. - split. + unfold isbinopfun. change (∏ x x' : commringfrac X (ringpossubmonoid X is1 is2), paths (g (x * x')) ((g x) * (g x'))). apply (setquotuniv2prop _ (λ x x' : commringfrac X (ringpossubmonoid X is1 is2), make_hProp _ (setproperty (fldfrac X is) (g (x * x')) ((g x) * (g x'))))). intros xa1 xa2. change (paths (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (g0 (commringfracop2int X (ringpossubmonoid X is1 is2) xa1 xa2))) (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (commringfracop2int X (intdomnonzerosubmonoid X) (g0 xa1) (g0 xa2)))). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. unfold commringfracop2int. unfold abmonoidfracopint. simpl. apply (pathsdirprod). * apply idpath. * destruct xa1 as [ x1 aa1 ]. destruct xa2 as [ x2 aa2 ]. simpl. destruct aa1 as [ a1 ia1 ]. destruct aa2 as [ a2 ia2 ]. simpl. apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (tpair _ (a1 * a2) (rtoneq ir (is1 a1 a2 ia1 ia2))) (make_carrier (λ x : pr1 X, make_hProp (x = 0 -> empty) (isapropneg (x = 0))) (a1 * a2) (fun e : paths (a1 * a2) 0 => toneghdisj (make_dirprod (rtoneq ir ia1) (rtoneq ir ia2)) (intdomax X a1 a2 e))) (idpath _)). + change (paths (setquotpr (eqrelcommringfrac X (intdomnonzerosubmonoid X)) (g0 (make_dirprod 1 (tpair _ 1 is2)))) (setquotpr _ (make_dirprod 1 (tpair _ 1 (nonzeroax X))))). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. simpl. apply pathsdirprod. * apply idpath. * apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (tpair _ 1 (rtoneq ir is2)) (tpair _ 1 (nonzeroax X))). simpl. apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings