proposition: Lemma orthogonal_split S beta : {X : 'CF(G) & X \in <<S>>%VS & {Y | [/\ beta = X + Y, '[X, Y] = 0 & orthogonal Y S]}}.
proof: Proof. suffices [X S_X [Y -> oYS]]: {X : _ & X \in <<S>>%VS & {Y | beta = X + Y & orthogonal Y S}}. - exists X => //; exists Y. by rewrite cfdotC (span_orthogonal oYS) ?memv_span1 ?conjC0. elim: S beta => [|phi S IHS] beta. by exists 0; last exists beta; rewrite ?mem0v ?add0r. have [[U S_U [V -> oVS]] [X S_X [Y -> oYS]]] := (IHS phi, IHS beta). pose Z := '[Y, V] / '[V] *: V; exists (X + Z). rewrite /Z -{4}(addKr U V) scalerDr scalerN addrA addrC span_cons. by rewrite memv_add ?memvB ?memvZ ?memv_line. exists (Y - Z); first by rewrite addrCA !addrA addrK addrC. apply/orthoPl=> psi /[!inE] /predU1P[-> | Spsi]; last first. by rewrite cfdotBl cfdotZl (orthoPl oVS _ Spsi) mulr0 subr0 (orthoPl oYS). rewrite cfdotBl !cfdotDr (span_orthogonal oYS) // ?memv_span ?mem_head //. rewrite !cfdotZl (span_orthogonal oVS _ S_U) ?mulr0 ?memv_span ?mem_head //. have [-> | nzV] := eqVneq V 0; first by rewrite cfdot0r !mul0r subrr. by rewrite divfK ?cfnorm_eq0 ?subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)