let i be Nat; :: thesis: for r being Real
for u, v being Element of ()
for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u holds
(N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf)

let r be Real; :: thesis: for u, v being Element of ()
for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u holds
(N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf)

let u, v be Element of (); :: thesis: for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u holds
(N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf)

let pf, uf be FinSequence of F_Real; :: thesis: for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u holds
(N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf)

let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & u = uf & pf = v & r <> 0 & v = r * u implies (N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf) )
assume that
A1: i in Seg 3 and
A2: u = uf and
A3: pf = v and
A4: r <> 0 and
A5: v = r * u ; :: thesis: (N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf)
set b = 1 / r;
reconsider s1 = uf . 1, s2 = uf . 2, s3 = uf . 3 as Element of F_Real by XREAL_0:def 1;
u in TOP-REAL 3 ;
then A6: u in REAL 3 by EUCLID:22;
A7: width <*uf*> = len u by
.= 3 by ;
A8: width N = 3 by MATRIX_0:24
.= len (<*uf*> @) by ;
N * (<*uf*> @) is Matrix of 3,1,F_Real by ;
then A9: ( [1,1] in Indices (N * (<*uf*> @)) & [2,1] in Indices (N * (<*uf*> @)) & [3,1] in Indices (N * (<*uf*> @)) ) by ;
reconsider t1 = v . 1, t2 = v . 2, t3 = v . 3 as Element of F_Real by XREAL_0:def 1;
A10: ( len N = 3 & width N = 3 ) by MATRIX_0:23;
A11: now :: thesis: ( len (Line (N,1)) = 3 & (Line (N,1)) . 1 = N * (1,1) & (Line (N,1)) . 2 = N * (1,2) & (Line (N,1)) . 3 = N * (1,3) )
thus len (Line (N,1)) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ; :: thesis: ( (Line (N,1)) . 1 = N * (1,1) & (Line (N,1)) . 2 = N * (1,2) & (Line (N,1)) . 3 = N * (1,3) )
( 1 in Seg () & 2 in Seg () & 3 in Seg () ) by ;
hence ( (Line (N,1)) . 1 = N * (1,1) & (Line (N,1)) . 2 = N * (1,2) & (Line (N,1)) . 3 = N * (1,3) ) by MATRIX_0:def 7; :: thesis: verum
end;
A12: now :: thesis: ( len (Line (N,2)) = 3 & (Line (N,2)) . 1 = N * (2,1) & (Line (N,2)) . 2 = N * (2,2) & (Line (N,2)) . 3 = N * (2,3) )
thus len (Line (N,2)) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ; :: thesis: ( (Line (N,2)) . 1 = N * (2,1) & (Line (N,2)) . 2 = N * (2,2) & (Line (N,2)) . 3 = N * (2,3) )
( 1 in Seg () & 2 in Seg () & 3 in Seg () ) by ;
hence ( (Line (N,2)) . 1 = N * (2,1) & (Line (N,2)) . 2 = N * (2,2) & (Line (N,2)) . 3 = N * (2,3) ) by MATRIX_0:def 7; :: thesis: verum
end;
A13: now :: thesis: ( len (Line (N,3)) = 3 & (Line (N,3)) . 1 = N * (3,1) & (Line (N,3)) . 2 = N * (3,2) & (Line (N,3)) . 3 = N * (3,3) )
thus len (Line (N,3)) = width N by MATRIX_0:def 7
.= 3 by MATRIX_0:23 ; :: thesis: ( (Line (N,3)) . 1 = N * (3,1) & (Line (N,3)) . 2 = N * (3,2) & (Line (N,3)) . 3 = N * (3,3) )
( 1 in Seg () & 2 in Seg () & 3 in Seg () ) by ;
hence ( (Line (N,3)) . 1 = N * (3,1) & (Line (N,3)) . 2 = N * (3,2) & (Line (N,3)) . 3 = N * (3,3) ) by MATRIX_0:def 7; :: thesis: verum
end;
3 = len uf by ;
then A14: uf = <*s1,s2,s3*> by FINSEQ_1:45;
A15: not not i = 1 & ... & not i = 3 by ;
A16: (1 / r) * v = ((1 / r) * r) * uf by
.= 1 * uf by
.= uf by RVSUM_1:52 ;
uf in TOP-REAL 3 by A2;
then A17: uf in REAL 3 by EUCLID:22;
v in TOP-REAL 3 ;
then A18: v in REAL 3 by EUCLID:22;
then |[((1 / r) * (v . 1)),((1 / r) * (v . 2)),((1 / r) * (v . 3))]| = uf by
.= |[(uf . 1),(uf . 2),(uf . 3)]| by ;
then A19: ( (1 / r) * (v . 1) = uf . 1 & (1 / r) * (v . 2) = uf . 2 & (1 / r) * (v . 3) = uf . 3 ) by FINSEQ_1:78;
A20: pf = <*t1,t2,t3*> by ;
(N * (<*uf*> @)) * (i,1) = (Line (N,i)) "*" (Col ((<*uf*> @),1)) by
.= (Line (N,i)) "*" uf by ANPROJ_8:93
.= <*(N * (i,1)),(N * (i,2)),(N * (i,3))*> "*" <*s1,s2,s3*> by
.= (((N * (i,1)) * s1) + ((N * (i,2)) * s2)) + ((N * (i,3)) * s3) by ANPROJ_8:7
.= (1 / r) * ((((N * (i,1)) * t1) + ((N * (i,2)) * t2)) + ((N * (i,3)) * t3)) by A19
.= (1 / r) * (<*(N * (i,1)),(N * (i,2)),(N * (i,3))*> "*" <*t1,t2,t3*>) by ANPROJ_8:7
.= (1 / r) * ((Line (N,i)) "*" pf) by ;
hence (N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf) ; :: thesis: verum