proposition: Lemma Lemma5 : Eigen1Vec R[i] 2.
proof: Proof. move=> m V HrV f f_stabV. suff: exists a, eigenvalue (restrict V f) a. by move=> [a /eigenvalue_restrict Hf]; exists a; apply: Hf. move: (\rank V) (restrict V f) => {f f_stabV V m} n f in HrV *. pose u := map_mx (@Re R) f; pose v := map_mx (@Im R) f. have fE : f = MtoC u + 'i%C *: MtoC v. rewrite /u /v [f]lock; apply/matrixP => i j; rewrite !mxE /=. by case: (locked f i j) => a b; simpc. move: u v => u v in fE *. pose L1fun : 'M[R]_n -> _ := 2%:R^-1 \*: (mulmxr u \+ (mulmxr v \o trmx) \+ ((mulmx (u^T)) \- (mulmx (v^T) \o trmx))). pose L1 := lin_mx [linear of L1fun]. pose L2fun : 'M[R]_n -> _ := 2%:R^-1 \*: (((@GRing.opp _) \o (mulmxr u \o trmx) \+ mulmxr v) \+ ((mulmx (u^T) \o trmx) \+ (mulmx (v^T)))). pose L2 := lin_mx [linear of L2fun]. have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _). + by move: HrV; rewrite mxrank1 !dvdn2 ?negbK oddM andbb. + by move=> ? _ /=; rewrite submx1. + suff {f fE}: L1 *m L2 = L2 *m L1. move: L1 L2 => L1 L2 commL1L2 La Lb. rewrite !{1}in_cons !{1}in_nil !{1}orbF. by move=> /orP [] /eqP -> /orP [] /eqP -> //; symmetry. apply/eqP/mulmxP => x; rewrite [X in X = _]mulmxA [X in _ = X]mulmxA. rewrite 4!mul_rV_lin !mxvecK /= /L1fun /L2fun /=; congr (mxvec (_ *: _)). move=> {L1 L2 L1fun L2fun}. case: n {x} (vec_mx x) => [//|n] x in HrV u v *. do ?[rewrite -(scalemxAl, scalemxAr, scalerN, scalerDr) |rewrite (mulmxN, mulNmx, trmxK, trmx_mul) |rewrite ?[(_ *: _)^T]linearZ ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=]. congr (_ *: _). rewrite !(mulmxDr, mulmxDl, mulNmx, mulmxN, mulmxA, opprD, opprK). do ![move: (_ *m _ *m _)] => t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12. rewrite [X in X + _ + _]addrC [X in X + _ = _]addrACA. rewrite [X in _ = (_ + _ + X) + _]addrC [X in _ = X + _]addrACA. rewrite [X in _ + (_ + _ + X) = _]addrC [X in _ + X = _]addrACA. rewrite [X in _ = _ + (X + _)]addrC [X in _ = _ + X]addrACA. rewrite [X in X = _]addrACA [X in _ = X]addrACA; congr (_ + _). by rewrite addrC [X in X + _ = _]addrACA [X in _ + X = _]addrACA. move=> g g_neq0 Hg; have [] := (Hg L1, Hg L2). rewrite !(mem_head, in_cons, orbT) => []. move=> [//|a /eigenspaceP g_eigenL1] [//|b /eigenspaceP g_eigenL2]. rewrite !mul_rV_lin /= /L1fun /L2fun /= in g_eigenL1 g_eigenL2. do [move=> /(congr1 vec_mx); rewrite mxvecK linearZ /=] in g_eigenL1. do [move=> /(congr1 vec_mx); rewrite mxvecK linearZ /=] in g_eigenL2. move=> {L1 L2 L1fun L2fun Hg HrV}. set vg := vec_mx g in g_eigenL1 g_eigenL2. exists (a +i* b); apply/eigenvalueP. pose w := (MtoC vg - 'i%C *: MtoC vg^T). exists (nz_row w); last first. rewrite nz_row_eq0 subr_eq0; apply: contraNneq g_neq0 => Hvg. rewrite -vec_mx_eq0; apply/eqP/matrixP => i j; rewrite !mxE /=. move: Hvg => /matrixP /(_ i j); rewrite !mxE /=; case. by rewrite !(mul0r, mulr0, add0r, mul1r, oppr0) => ->. apply/eigenspaceP. case: n f => [|n] f in u v g g_neq0 vg w fE g_eigenL1 g_eigenL2 *. by rewrite thinmx0 eqxx in g_neq0. rewrite (submx_trans (nz_row_sub _)) //; apply/eigenspaceP. rewrite fE [a +i* b]complexE /=. rewrite !(mulmxDr, mulmxBl, =^~scalemxAr, =^~scalemxAl) -!map_mxM. rewrite !(scalerDl, scalerDr, scalerN, =^~scalemxAr, =^~scalemxAl). rewrite !scalerA /= mulrAC ['i%C * _]sqr_i ?mulN1r scaleN1r scaleNr !opprK. rewrite [_ * 'i%C]mulrC -!scalerA -!map_mxZ /=. rewrite ['i%C *: _ + _]addrC [LHS]addrACA ['i%C *: _ + _]addrC [RHS]addrACA. rewrite [X in _ + _ + X]addrC -scalerBr -!(rmorphB, rmorphD)/=. rewrite [- _ + _ in RHS]addrC -scalerBr -!(rmorphB, rmorphD)/=. congr (_ + 'i%C *: _); congr map_mx; rewrite -[_ *: _^T]linearZ /=; rewrite -g_eigenL1 -g_eigenL2 linearZ -(scalerDr, scalerBr); do ?rewrite ?trmxK ?trmx_mul ?[(_ + _)^T]linearD ?[(- _)^T]linearN /=; rewrite -[in X in _ *: (_ + X)]addrC 1?opprD 1?opprB ?mulmxN ?mulNmx; rewrite [X in _ *: X]addrACA. rewrite -mulr2n [X in _ *: (_ + X)]addrACA subrr addNr !addr0. by rewrite -scaler_nat scalerA mulVf ?pnatr_eq0 // scale1r. rewrite subrr addr0 addrA addrAC -addrA -mulr2n addrC. by rewrite -scaler_nat scalerA mulVf ?pnatr_eq0 // scale1r. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)