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. 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), 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 (setquotpr _ (g0 (commringfracop1int _ _ xa1 xa2)) = setquotpr (eqrelcommringfrac _ _) (commringfracop1int X _ (g0 xa1) (g0 xa2))). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. unfold commringfracop1int. simpl. apply (pathsdirprod). * apply idpath. * induction xa1 as [ x1 aa1 ]. induction xa2 as [ x2 aa2 ]. simpl. induction aa1 as [ a1 ia1 ]. induction aa2 as [ a2 ia2 ]. simpl. apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (a1 * a2 ,, rtoneq ir (is1 a1 a2 ia1 ia2)) (make_carrier (λ x : pr1 X, make_hProp (x = 0 → empty) (isapropneg (x = 0))) (a1 * a2) (λ (e : a1 * a2 = 0), toneghdisj (rtoneq ir ia1 ,, rtoneq ir ia2) (intdomax X a1 a2 e))) (idpath _)). + change (setquotpr (eqrelcommringfrac X _) (g0 (0 ,, 1 ,, is2)) = setquotpr _ (0 ,, 1 ,, nonzeroax X)). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. simpl. apply pathsdirprod. * apply idpath. * apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (1 ,, rtoneq ir is2) (1 ,, nonzeroax X)). simpl. apply idpath. - split. + unfold isbinopfun. change (∏ x x' : commringfrac X (ringpossubmonoid X is1 is2), 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 (setquotpr _ (g0 (commringfracop2int _ _ xa1 xa2)) = setquotpr (eqrelcommringfrac _ _) (commringfracop2int X _ (g0 xa1) (g0 xa2))). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. unfold commringfracop2int. unfold abmonoidfracopint. simpl. apply (pathsdirprod). * apply idpath. * induction xa1 as [ x1 aa1 ]. induction xa2 as [ x2 aa2 ]. simpl. induction aa1 as [ a1 ia1 ]. induction aa2 as [ a2 ia2 ]. simpl. apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (a1 * a2 ,, rtoneq ir (is1 a1 a2 ia1 ia2)) (make_carrier (λ x : pr1 X, make_hProp (x = 0 → empty) (isapropneg (x = 0))) (a1 * a2) (λ (e : a1 * a2 = 0), toneghdisj (rtoneq ir ia1 ,, rtoneq ir ia2) (intdomax X a1 a2 e))) (idpath _)). + change (setquotpr (eqrelcommringfrac _ _) (g0 (1 ,, 1 ,, is2)) = setquotpr _ (1 ,, 1 ,, nonzeroax X)). apply (maponpaths (setquotpr _)). unfold g0. unfold weqfldfracgtint_b. simpl. apply pathsdirprod. * apply idpath. * apply (invmaponpathsincl (@pr1 _ _) (isinclpr1 _ (λ a, (isapropneg (a = 0)))) (1 ,, rtoneq ir is2) (1 ,, nonzeroax X)). simpl. apply idpath. Qed.
Require Import UniMath.Algebra.Groups.