proposition: Corollary orthonormal_vchar_diff_ortho (X : {group gT}) (a b c d : 'CF(X)) : {subset a :: b <= 'Z[irr X]} /\ {subset c :: d <= 'Z[irr X]} -> orthonormal (a :: b) && orthonormal (c :: d) -> [&& '[a - b, c - d] == 0, (a - b) 1%g == 0 & (c - d) 1%g == 0] -> '[a, c] = 0.
proof: Proof. move=> Zabcd Oabcd; rewrite -[c - d]scale1r scalerBr. move/(vchar_pairs_orthonormal Zabcd Oabcd) => /implyP. rewrite rpred1 oner_eq0 (orthonormal_cat (a :: b)) /=. by case/and3P=> _ _ /andP[] /andP[] /eqP. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)