let i be Nat; 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; 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); 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; 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; ( 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
; (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 ( 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
;
( (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;
verum end;
A12:
now ( 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
;
( (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;
verum end;
A13:
now ( 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
;
( (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;
verum end;
3 = len uf
by A2, A6, EUCLID_8:50;
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)
; verum