proposition: Lemma orsum_invariant1 r r' f g g': order_on r (domain g) -> order_on r' (domain g') -> order_isomorphism f r r' -> (forall i, inc i (substrate r) -> (Vg g i) \Is (Vg g' (Vf f i))) -> (order_sum r g) \Is (order_sum r' g').
proof: Proof. move=> [or sr] [or' sr'] oi ali. have oa: (orsum_ax r g). by split => //; hnf;rewrite - sr=> i idg; move:(ali _ idg)=> [h []]. move: (oi) => [_ _ [[[ff ijf] sjf] srf tgf] oif]. have oa': orsum_ax r' g'. split => //; hnf;rewrite - sr' - tgf=> i idg. move: ((proj2 sjf) _ idg) => [x xsf ->]. by rewrite srf in xsf; move: (ali _ xsf)=> [h [o1 o2 _]]. move: (orsum_or oa) (orsum_or oa') => h1 h2; aw. set fa := fam_of_substrates g. set fb := fam_of_substrates g'. pose oj i := choose (fun z => order_isomorphism z (Vg g i) (Vg g' (Vf f i))). have ojp: (forall i, inc i (substrate r) -> order_isomorphism (oj i) (Vg g i) (Vg g' (Vf f i))). move=> i isr; rewrite /oj; apply: (choose_pr (ali _ isr)). pose h x := J (Vf (oj (Q x)) (P x)) (Vf f (Q x)). have ta: (forall x, inc x (disjointU fa) -> inc (h x) (disjointU fb)). move=> x xd; case: (disjointU_hi xd); rewrite /fa/fam_of_substrates. rewrite Lgd => qd; rewrite LgV // => ps px. have wq: (inc (Vf f (Q x)) (domain g')). by rewrite - sr' - tgf; Wtac; rewrite srf sr. apply: disjointU_pi; rewrite /fb ? fos_d // LgV //. rewrite sr in ojp;move: (ojp _ qd) => [_ _ [fx sx tx] _]. by rewrite - tx; Wtac; fct_tac. have ta1: lf_axiom h (substrate (order_sum r g)) (substrate(order_sum r' g')). by rewrite !orsum_sr. exists (Lf h (substrate (order_sum r g)) (substrate (order_sum r' g'))). hnf; rewrite /bijection_prop lf_source lf_target; split => //. rewrite !orsum_sr //; split=> //; apply: lf_bijective =>//. rewrite /h => u v us vs eq. move:(du_index_pr1 us) (du_index_pr1 vs)=> [Qu Pu pu][Qv Pv pv]. move: (pr2_def eq) (pr1_def eq) => r1 r2. have sQ: Q u = Q v by apply: ijf => //; rewrite srf;ue. rewrite - sQ in r2 Pv; rewrite - sr in Qu. move: (ojp _ Qu) => [_ _ [[[_ ijfj] _] sfj _] _]. apply: pair_exten =>//; apply: ijfj =>//; ue. move=> y ys; move: (du_index_pr1 ys)=> [Qy Py py]. rewrite - sr' -tgf in Qy; move:((proj2 sjf) _ Qy) =>[x xsf Wx]. rewrite srf in xsf; move: (ojp _ xsf) => [_ _ [[_ sjj] sfj tjj] _]. rewrite Wx - tjj in Py; move: ((proj2 sjj) _ Py)=> [x0 x0s x0w]. have xdg: inc x (domain g) by ue. exists (J x0 x). apply: disjointU_pi; aw; trivial;rewrite LgV //; ue. by rewrite /h; aw; rewrite -Wx -x0w; aw; rewrite py. hnf;aw; rewrite !orsum_sr // => x y xs ys; rewrite !LfV//. move: ta1; rewrite ! orsum_sr // => ta2; move: (ta2 _ xs)(ta2 _ ys) => ha hb. move: (du_index_pr1 xs) (du_index_pr1 ys) => [Qx Px px][Qy Py py]. rewrite - sr - srf in Qx Qy; rewrite - srf in ojp. move: (ojp _ Qx) => [_ _ [_ sfj _] ojj]. have qa: inc (P x) (source (oj (Q x))) by ue. have qb: Q x = Q y -> inc (P y) (source (oj (Q x))) by rewrite sfj => ->. split; move/orsum_gleP => [_ _ aux]; apply /orsum_gleP;split => //; move: aux; rewrite /order_sum_r /h !pr1_pair !pr2_pair. case => pa; first by left; apply /(order_isomorphism_siso oi Qx Qy). move: pa => [pa pb];rewrite - pa; right; split => //. by apply/ojj => //; apply: qb. case => pa; first by left; apply /(order_isomorphism_siso oi Qx Qy). move: pa => [pa]; move: (ijf _ _ Qx Qy pa) => pc; rewrite - pc => pb. by right;split => //; apply /ojj => //; apply: qb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)