let N be invertible Matrix of 3,F_Real; :: thesis: for u, mu being Element of (TOP-REAL 3)
for uf being FinSequence of F_Real
for ut being FinSequence of 1 -tuples_on REAL st not u is zero & u = uf & ut = N * uf & mu = M2F ut holds
not mu is zero
let u, mu be Element of (TOP-REAL 3); :: thesis: for uf being FinSequence of F_Real
for ut being FinSequence of 1 -tuples_on REAL st not u is zero & u = uf & ut = N * uf & mu = M2F ut holds
not mu is zero
let uf be FinSequence of F_Real; :: thesis: for ut being FinSequence of 1 -tuples_on REAL st not u is zero & u = uf & ut = N * uf & mu = M2F ut holds
not mu is zero
let ut be FinSequence of 1 -tuples_on REAL; :: thesis: ( not u is zero & u = uf & ut = N * uf & mu = M2F ut implies not mu is zero )
assume that
A1: not u is zero and
A2: u = uf and
A3: ut = N * uf and
A4: mu = M2F ut ; :: thesis: not mu is zero
uf in TOP-REAL 3 by A2;
then A5: uf in REAL 3 by EUCLID:22;
A6: len uf = 3 by A5, EUCLID_8:50;
A7: width <*uf*> = 3 by A6, Th61;
then A8: len (<*uf*> @) = width <*uf*> by MATRIX_0:29
.= len uf by MATRIX_0:23 ;
then A9: len (<*uf*> @) = 3 by A5, EUCLID_8:50;
A10: len <*uf*> = 1 by MATRIX_0:23;
then A11: ( len (<*uf*> @) = 3 & width (<*uf*> @) = 1 ) by A7, MATRIX_0:29;
width N = 3 by MATRIX_0:24;
then ( len (N * (<*uf*> @)) = len N & width (N * (<*uf*> @)) = width (<*uf*> @) ) by A11, MATRIX_3:def 4;
then A12: ( len (N * (<*uf*> @)) = 3 & width (N * (<*uf*> @)) = 1 ) by A10, A7, MATRIX_0:29, MATRIX_0:24;
A13: width N = 3 by MATRIX_0:24
.= len (<*uf*> @) by A8, A5, EUCLID_8:50 ;
A14: len ut = len (N * (<*uf*> @)) by A3, LAPLACE:def 9
.= len N by A13, MATRIX_3:def 4
.= 3 by MATRIX_0:23 ;
assume A15: mu is zero ; :: thesis: contradiction
reconsider MU = M2F ut as FinSequence of REAL ;
A16: ut = F2M MU by A14, Th69
.= <*<*0*>,<*0*>,<*0*>*> by A15, A4, EUCLID_5:4, Th65 ;
A17: N ~ is_reverse_of N by MATRIX_6:def 4;
A18: width (N ~) = 3 by MATRIX_0:24;
A19: ( len N = 3 & width N = 3 ) by MATRIX_0:24;
A20: (1. (F_Real,3)) * (<*uf*> @) = ((N ~) * N) * (<*uf*> @) by A17, MATRIX_6:def 2
.= (N ~) * (N * (<*uf*> @)) by A9, A18, A19, MATRIX_3:33 ;
A21: N * (<*uf*> @) is Matrix of 3,1,F_Real by A12, MATRIX_0:20;
N * (<*uf*> @) = <*<*0*>,<*0*>,<*0*>*> by LAPLACE:def 9, A3, A16;
then (N ~) * (N * (<*uf*> @)) = <*<*0*>,<*0*>,<*0*>*> by Th7, A21;
then <*uf*> @ = <*<*0*>,<*0*>,<*0*>*> by A20, Th80, A5, EUCLID_8:50;
hence contradiction by A1, A2, Th81; :: thesis: verum