let N be invertible Matrix of 3,F_Real; 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); 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; 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; ( 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
; 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
; 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; verum