proposition: Lemma isometry_of_cfnorm S tauS : pairwise_orthogonal S -> pairwise_orthogonal tauS -> map cfnorm tauS = map cfnorm S -> {tau : {linear 'CF(L) -> 'CF(G)} | map tau S = tauS & {in <<S>>%VS &, isometry tau}}.
proof: Proof. move=> oS oT eq_nST; have freeS := orthogonal_free oS. have eq_sz: size tauS = size S by have:= congr1 size eq_nST; rewrite !size_map. have [tau defT] := linear_of_free S tauS; rewrite -[S]/(tval (in_tuple S)). exists tau => [|u v /coord_span-> /coord_span->]; rewrite ?raddf_sum ?defT //=. apply: eq_bigr => i _ /=; rewrite linearZ !cfdotZr !cfdot_suml; congr (_ * _). apply: eq_bigr => j _ /=; rewrite linearZ !cfdotZl; congr (_ * _). rewrite -!(nth_map 0 0 tau) ?{}defT //; have [-> | neq_ji] := eqVneq j i. by rewrite -!['[_]](nth_map 0 0 cfnorm) ?eq_sz // eq_nST. have{oS} [/=/andP[_ uS] oS] := pairwise_orthogonalP oS. have{oT} [/=/andP[_ uT] oT] := pairwise_orthogonalP oT. by rewrite oS ?oT ?mem_nth ?nth_uniq ?eq_sz. 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)