proposition: Lemma orprod_invariant1 r r' f g g': worder_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_prod r g) \Is (order_prod r' g').
proof: Proof. move=> [wor sr] [or' sr'] oif ali. have aux: (r \Is r') by exists f. have wor':= (worder_invariance aux wor). clear aux. have bf: bijection f by move: oif => [_ _ [bf _ _] _]. move: (oif) => [or _ [[[ff ijf] sjf] srf tgf] oif']. have oa: (orprod_ax r g). by split => //;hnf;rewrite - sr=> i idg; move:(ali _ idg)=> [h [o1 o2 _]]. have oa': orprod_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: (orprod_or oa)(orprod_or oa') => o1 o2; aw. set fa := fam_of_substrates g. set fb := fam_of_substrates g'. pose oi i := choose (fun z => order_isomorphism z (Vg g i) (Vg g' (Vf f i))). have oip: (forall i, inc i (substrate r) -> order_isomorphism (oi i) (Vg g i) (Vg g' (Vf f i))). by move=> i isr; apply: (choose_pr (ali _ isr)). pose fi := Vf (inverse_fun f). have fip: (forall i, inc i (substrate r') -> Vf f (fi i) = i). move=> i isr; rewrite inverse_V //; ue. have fis: (forall i, inc i (substrate r') -> inc (fi i) (substrate r)). rewrite - tgf - srf; move=> i isf; apply:inverse_Vis =>//. pose fj := Vf f. have fjs: forall i, inc i (substrate r) -> (inc (fj i) (substrate r')). rewrite - srf - tgf /fj; move=> i isg; fprops. have fij: forall i, inc i (substrate r) -> fi (fj i) = i. rewrite - srf /fi/fj;move => i idf; rewrite inverse_V2 //. pose h z := Lg (substrate r') (fun i => Vf (oi (fi i))(Vg z (fi i)) ). set (A := substrate(order_prod r g)). set (B := substrate(order_prod r' g')). have HA : A = (prod_of_substrates g) by rewrite /A orprod_sr. have HB : B = (prod_of_substrates g') by rewrite /B orprod_sr. have ta: (forall z, inc z A -> inc (h z) B). rewrite HA HB => z /prod_of_substratesP [fgf dz iVV]. apply /prod_of_substratesP; rewrite /h;split => //; [fprops | by aw | ]. rewrite - sr' => i isr; rewrite LgV//. have fisr:= (fis _ isr). move: (oip _ fisr) => [_ _ [boi soi]]. rewrite (fip _ isr) => <- _; Wtac; try fct_tac. by rewrite soi; apply: iVV; rewrite - sr. have ta': (forall w, inc w B -> exists2 z, inc z A & w = h z). rewrite HA HB; move => w /prod_of_substratesP [fgf dz iVV]. exists (Lg (substrate r) (fun i => Vf (inverse_fun (oi i))(Vg w (fj i)))). apply /prod_of_substratesP;split => //; [ fprops | by aw | ]. rewrite - sr => i isr; rewrite LgV//. move: (oip _ isr) => [_ _ [boi soi toi] _ ]. rewrite - soi; apply: inverse_Vis =>//; rewrite toi. apply: iVV; rewrite - sr'; apply: (fjs _ isr). rewrite /h; apply: fgraph_exten; [ exact | fprops | by aw ; ue | ]. rewrite dz - sr'; move=> x xdw /=; move: (fis _ xdw) => fisr. rewrite !LgV //; move: (oip _ fisr) => [_ _ [boi soi toi] _ ]. rewrite /fj (fip _ xdw) inverse_V // toi (fip _ xdw); apply: iVV; ue. have hi: (forall z z', inc z A -> inc z' A -> h z = h z' -> z = z'). rewrite HA => z z' zA zA' p3; apply: (setXb_exten zA zA'). hnf; aw;move=> i idg; move: (prod_of_substrates_p zA idg) =>p4. have p5 := (prod_of_substrates_p zA' idg). rewrite - sr in idg; move: (fij _ idg)(fjs _ idg) => p6 p7. move: (f_equal (Vg ^~(fj i)) p3); rewrite /h !LgV // p6. move: (oip _ idg) => [_ _ [[[_ ioi] _] soi toi] _ ]. apply: ioi; ue. have ta2: (lf_axiom h A B) by []. exists (Lf h A B). split => //; [ by saw;apply: lf_bijective | hnf; aw]. move=> x y xA yA; rewrite !LfV //; split. move /(orprod_gleP oa) => [_ _ ha]; apply /(orprod_gleP oa'). rewrite -HB; split => //; try apply: ta =>//; case:ha => ha. by left; rewrite ha. move: ha => [j [jst jlt ieq]]; right. move: (fjs _ jst)(fij _ jst) => fjst fijt; rewrite /h;ex_tac. by rewrite !LgV// fijt; apply: (order_isomorphism_sincr (oip _ jst)). move=> i ifj. have isr: inc i (substrate r') by order_tac. rewrite !LgV // (ieq (fi i)) // - fijt; apply /(order_isomorphism_siso oif); [by rewrite srf; apply: fis | ue | rewrite ! fip //]. move /(orprod_gleP oa') => [_ _ ha]; apply /(orprod_gleP oa). rewrite - HA;split => //. case:ha=> aux; first by left; apply: hi. right; move: aux => [j [jsr jlt jle]]. move: (fip _ jsr)(fis _ jsr) => fipa fisa. ex_tac. move: (oip _ fisa) => [_ _ [_ soi toi] _ ]. apply /(order_isomorphism_siso (oip _ fisa)); try (rewrite soi; apply: prod_of_substrates_p; ue); move: jlt; rewrite /h fipa; rewrite !LgV //. move=> i lti. have isr: inc i (substrate r) by order_tac. move: (isr) => isr1. move: (oip _ isr) => [_ _ [[[_ ioi] _] soi toi] _ ]. apply: ioi. move: xA isr; rewrite soi sr HA; apply: prod_of_substrates_p. move: yA isr; rewrite soi sr HA; apply: prod_of_substrates_p. rewrite - srf in isr fisa. move /(order_isomorphism_siso oif isr fisa): lti; rewrite fip // => aux. by move: (jle _ aux); rewrite /h ! LgV//; try order_tac; rewrite fij //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)