proposition: Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R) (op : Monoid.com_law idx) (A : I -> set T) (F : set T -> R) : finite_set D -> trivIset D A -> F set0 = idx -> \big[op/idx]_(i <- fset_set D) F (A i) = \big[op/idx]_(X <- (A @` fset_set D)%fset) F X.
proof: Proof. elim/Pchoice: R => R in idx op F *. move=> Dfin Atriv F0; symmetry. pose D' := [fset i in fset_set D | A i != set0]%fset. transitivity (\big[op/idx]_(X <- (A @` D')%fset) F X). apply: perm_big_supp; rewrite uniq_perm ?filter_uniq//=. move=> X; rewrite !mem_filter; case: (eqVneq (F X) idx) => //= FXNidx. apply/imfsetP/imfsetP=> -[i/=]; rewrite ?(inE, in_fset_set)//=. move=> Di XAi; exists i; rewrite // !(inE, in_fset_set)//=. by rewrite (mem_set Di)/= -XAi; apply: contra_neq FXNidx => ->. by move=> /andP[Di AiN0] XAi; exists i; rewrite ?in_fset_set. rewrite big_imfset//=; last first. move=> i j; rewrite !(inE, in_fset_set)//= => /andP[+ +] /andP[+ +]. rewrite !inE => Di /set0P[x Aix] Dj _ Aij. by apply: (Atriv _ _ Di Dj); exists x; split=> //; rewrite -Aij. apply: perm_big_supp; rewrite uniq_perm ?filter_uniq//= => i. rewrite !mem_filter; case: (eqVneq (F (A i)) idx) => //= FAiidx. rewrite !(in_fset_set, inE)//=; case: (boolP (i \in D)) => //= Di. by apply: contra_neq FAiidx => ->. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)