let i be Nat; :: thesis: for r being Real

for u, v being Element of (TOP-REAL 3)

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 (TOP-REAL 3)

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 (TOP-REAL 3); :: 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 A2, ANPROJ_8:75

.= 3 by A6, EUCLID_8:50 ;

A8: width N = 3 by MATRIX_0:24

.= len (<*uf*> @) by MATRIX_0:def 6, A7 ;

N * (<*uf*> @) is Matrix of 3,1,F_Real by A2, FINSEQ_3:153, ANPROJ_8:91;

then A9: ( [1,1] in Indices (N * (<*uf*> @)) & [2,1] in Indices (N * (<*uf*> @)) & [3,1] in Indices (N * (<*uf*> @)) ) by MATRIX_0:23, ANPROJ_8:2;

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;

then A14: uf = <*s1,s2,s3*> by FINSEQ_1:45;

A15: not not i = 1 & ... & not i = 3 by A1, FINSEQ_1:91;

A16: (1 / r) * v = ((1 / r) * r) * uf by A5, A2, RVSUM_1:49

.= 1 * uf by A4, XCMPLX_1:87

.= 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 A16, EUCLID_8:52

.= |[(uf . 1),(uf . 2),(uf . 3)]| by A17, EUCLID_8:1 ;

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 A3, A18, EUCLID_8:1;

(N * (<*uf*> @)) * (i,1) = (Line (N,i)) "*" (Col ((<*uf*> @),1)) by A15, A8, A9, MATRIX_3:def 4

.= (Line (N,i)) "*" uf by ANPROJ_8:93

.= <*(N * (i,1)),(N * (i,2)),(N * (i,3))*> "*" <*s1,s2,s3*> by A15, A11, A12, A13, FINSEQ_1:45, A14

.= (((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 A15, A11, A12, A13, FINSEQ_1:45, A20 ;

hence (N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf) ; :: thesis: verum

for u, v being Element of (TOP-REAL 3)

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 (TOP-REAL 3)

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 (TOP-REAL 3); :: 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 A2, ANPROJ_8:75

.= 3 by A6, EUCLID_8:50 ;

A8: width N = 3 by MATRIX_0:24

.= len (<*uf*> @) by MATRIX_0:def 6, A7 ;

N * (<*uf*> @) is Matrix of 3,1,F_Real by A2, FINSEQ_3:153, ANPROJ_8:91;

then A9: ( [1,1] in Indices (N * (<*uf*> @)) & [2,1] in Indices (N * (<*uf*> @)) & [3,1] in Indices (N * (<*uf*> @)) ) by MATRIX_0:23, ANPROJ_8:2;

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 (width N) & 2 in Seg (width N) & 3 in Seg (width N) ) by A10, FINSEQ_1:1;

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;.= 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 (width N) & 2 in Seg (width N) & 3 in Seg (width N) ) by A10, FINSEQ_1:1;

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

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 (width N) & 2 in Seg (width N) & 3 in Seg (width N) ) by A10, FINSEQ_1:1;

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;.= 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 (width N) & 2 in Seg (width N) & 3 in Seg (width N) ) by A10, FINSEQ_1:1;

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

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) )

3 = len uf
by A2, A6, EUCLID_8:50;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 (width N) & 2 in Seg (width N) & 3 in Seg (width N) ) by A10, FINSEQ_1:1;

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 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 (width N) & 2 in Seg (width N) & 3 in Seg (width N) ) by A10, FINSEQ_1:1;

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

then A14: uf = <*s1,s2,s3*> by FINSEQ_1:45;

A15: not not i = 1 & ... & not i = 3 by A1, FINSEQ_1:91;

A16: (1 / r) * v = ((1 / r) * r) * uf by A5, A2, RVSUM_1:49

.= 1 * uf by A4, XCMPLX_1:87

.= 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 A16, EUCLID_8:52

.= |[(uf . 1),(uf . 2),(uf . 3)]| by A17, EUCLID_8:1 ;

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 A3, A18, EUCLID_8:1;

(N * (<*uf*> @)) * (i,1) = (Line (N,i)) "*" (Col ((<*uf*> @),1)) by A15, A8, A9, MATRIX_3:def 4

.= (Line (N,i)) "*" uf by ANPROJ_8:93

.= <*(N * (i,1)),(N * (i,2)),(N * (i,3))*> "*" <*s1,s2,s3*> by A15, A11, A12, A13, FINSEQ_1:45, A14

.= (((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 A15, A11, A12, A13, FINSEQ_1:45, A20 ;

hence (N * (<*uf*> @)) * (i,1) = (1 / r) * ((Line (N,i)) "*" pf) ; :: thesis: verum