proposition: Lemma vchar_pairs_orthonormal (X : {group gT}) (a b c d : 'CF(X)) u v : {subset (a :: b) <= 'Z[irr X]} /\ {subset (c :: d) <= 'Z[irr X]} -> orthonormal (a :: b) && orthonormal (c :: d) -> [&& u \is Creal, v \is Creal, u != 0 & v != 0] -> [&& '[a - b, u *: c - v *: d] == 0, (a - b) 1%g == 0 & (u *: c - v *: d) 1%g == 0] -> orthonormal [:: a; b; c; d].
proof: Proof. have osym2 (e f : 'CF(X)) : orthonormal (e :: f) -> orthonormal (f :: e). by rewrite !(orthonormal_cat [::_] [::_]) orthogonal_sym andbCA. have def_o f S: orthonormal (f :: S) -> '[f : 'CF(X)] = 1. by case/andP=> /andP[/eqP]. case=> /allP/and3P[Za Zb _] /allP/and3P[Zc Zd _] /andP[o_ab o_cd]. rewrite (orthonormal_cat (a :: b)) o_ab o_cd /=. case/and4P=> r_u r_v nz_u nz_v /and3P[o_abcd ab1 cd1]. wlog suff: a b c d u v Za Zb Zc Zd o_ab o_cd r_u r_v nz_u nz_v o_abcd ab1 cd1 / '[a, c]_X == 0. - move=> IH; rewrite /orthogonal /= !andbT (IH a b c d u v) //=. have vc_sym (e f : 'CF(X)) : ((e - f) 1%g == 0) = ((f - e) 1%g == 0). by rewrite -opprB cfunE oppr_eq0. have ab_sym e: ('[b - a, e] == 0) = ('[a - b, e] == 0). by rewrite -opprB cfdotNl oppr_eq0. rewrite (IH b a c d u v) // 1?osym2 1?vc_sym ?ab_sym //=. rewrite -oppr_eq0 -cfdotNr opprB in o_abcd. by rewrite (IH a b d c v u) ?(IH b a d c v u) // 1?osym2 1?vc_sym ?ab_sym. apply: contraLR cd1 => nz_ac. have [/orthonormal2P[ab0 a1 b1] /orthonormal2P[cd0 c1 d1]] := (o_ab, o_cd). have [ea [ia def_a]] := vchar_norm1P Za a1. have{nz_ac} [e defc]: exists e : bool, c = (-1) ^+ e *: a. have [ec [ic def_c]] := vchar_norm1P Zc c1; exists (ec (+) ea). move: nz_ac; rewrite def_a def_c scalerA; rewrite -signr_addb addbK. rewrite cfdotZl cfdotZr cfdot_irr mulrA mulrC mulf_eq0. by have [-> // | _]:= ia =P ic; rewrite eqxx. have def_vbd: v * '[b, d]_X = - ((-1) ^+ e * u). apply/eqP; have:= o_abcd; rewrite cfdotDl cfdotNl !raddfB /=. rewrite defc !cfdotZr a1 (cfdotC b) ab0 rmorph0 mulr1. rewrite -[a]scale1r -{2}[1]/((-1) ^+ false) -(addbb e) signr_addb -scalerA. rewrite -defc cfdotZl cd0 !mulr0 opprK addrA !subr0 mulrC addrC addr_eq0. by rewrite rmorph_sign !conj_Creal. have nz_bd: '[b, d] != 0. move/esym/eqP: def_vbd; apply: contraTneq => ->. by rewrite mulr0 oppr_eq0 mulf_eq0 signr_eq0. have{nz_bd} defd: d = '[b, d] *: b. move: nz_bd; have [eb [ib ->]] := vchar_norm1P Zb b1. have [ed [id ->]] := vchar_norm1P Zd d1. rewrite scalerA cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr. have [-> _ | _] := ib =P id; last by rewrite !mulr0 eqxx. by rewrite mulr1 mulrAC -!signr_addb addbb. rewrite defd scalerA def_vbd scaleNr opprK defc scalerA mulrC -raddfD cfunE. rewrite !mulf_neq0 ?signr_eq0 // -(subrK a b) -opprB addrCA 2!cfunE. rewrite (eqP ab1) oppr0 add0r cfunE -mulr2n -mulr_natl mulf_eq0 pnatr_eq0. by rewrite /= def_a cfunE mulf_eq0 signr_eq0 /= irr1_neq0. 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)