let uf be FinSequence of F_Real; ( len uf = 3 implies <*uf*> @ = (1. (F_Real,3)) * (<*uf*> @) )
assume A1:
len uf = 3
; <*uf*> @ = (1. (F_Real,3)) * (<*uf*> @)
then A2:
<*uf*> @ = <*<*(uf . 1)*>,<*(uf . 2)*>,<*(uf . 3)*>*>
by Th63;
then A3:
len (<*uf*> @) = 3
by FINSEQ_1:45;
set M = 1. (F_Real,3);
uf is 3 -element
by A1, CARD_1:def 7;
then A4:
uf in REAL 3
by EUCLID_9:2;
now ( len ((1. (F_Real,3)) * (<*uf*> @)) = 3 & ((1. (F_Real,3)) * (<*uf*> @)) . 1 = <*(uf . 1)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> )A5:
(1. (F_Real,3)) * (<*uf*> @) is
Matrix of 3,1,
F_Real
by A4, EUCLID_8:50, Th74;
hence
len ((1. (F_Real,3)) * (<*uf*> @)) = 3
by MATRIX_0:23;
( ((1. (F_Real,3)) * (<*uf*> @)) . 1 = <*(uf . 1)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> )thus
((1. (F_Real,3)) * (<*uf*> @)) . 1
= <*(uf . 1)*>
( ((1. (F_Real,3)) * (<*uf*> @)) . 2 = <*(uf . 2)*> & ((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*> )proof
1
in Seg 3
by FINSEQ_1:1;
then A6:
((1. (F_Real,3)) * (<*uf*> @)) . 1
= Line (
((1. (F_Real,3)) * (<*uf*> @)),1)
by A5, MATRIX_0:52;
now ( len (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) = 1 & (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = uf . 1 )thus len (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) =
width ((1. (F_Real,3)) * (<*uf*> @))
by MATRIX_0:def 7
.=
1
by A5, MATRIX_0:23
;
(Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 = uf . 1thus
(Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1
= uf . 1
verumproof
A7:
[1,1] in Indices ((1. (F_Real,3)) * (<*uf*> @))
by A5, MATRIX_0:23, Th2;
A8:
width (1. (F_Real,3)) = len (<*uf*> @)
by A3, MATRIX_0:23;
reconsider a1 = 1,
a2 =
0 as
Element of
F_Real ;
A9:
(
Line (
(1. (F_Real,3)),1)
= <*a1,a2,a2*> &
uf = <*(uf . 1),(uf . 2),(uf . 3)*> )
by Th56, A1, FINSEQ_1:45;
dom uf = Seg 3
by A1, FINSEQ_1:def 3;
then reconsider uf1 =
uf . 1,
uf2 =
uf . 2,
uf3 =
uf . 3 as
Element of
F_Real by FINSEQ_1:1, FINSEQ_2:11;
A10:
(Line ((1. (F_Real,3)),1)) "*" uf =
((a1 * uf1) + (a2 * uf2)) + (a2 * uf3)
by A9, Th6
.=
uf . 1
;
1
in Seg 1
by FINSEQ_1:1;
then
1
in Seg (width ((1. (F_Real,3)) * (<*uf*> @)))
by A5, MATRIX_0:23;
then (Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1 =
((1. (F_Real,3)) * (<*uf*> @)) * (1,1)
by MATRIX_0:def 7
.=
(Line ((1. (F_Real,3)),1)) "*" (Col ((<*uf*> @),1))
by A7, A8, MATRIX_3:def 4
.=
(Line ((1. (F_Real,3)),1)) "*" uf
by Th76
;
hence
(Line (((1. (F_Real,3)) * (<*uf*> @)),1)) . 1
= uf . 1
by A10;
verum
end; end;
hence
((1. (F_Real,3)) * (<*uf*> @)) . 1
= <*(uf . 1)*>
by A6, FINSEQ_1:40;
verum
end; thus
((1. (F_Real,3)) * (<*uf*> @)) . 2
= <*(uf . 2)*>
((1. (F_Real,3)) * (<*uf*> @)) . 3 = <*(uf . 3)*>proof
2
in Seg 3
by FINSEQ_1:1;
then A11:
((1. (F_Real,3)) * (<*uf*> @)) . 2
= Line (
((1. (F_Real,3)) * (<*uf*> @)),2)
by A5, MATRIX_0:52;
now ( len (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) = 1 & (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = uf . 2 )thus len (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) =
width ((1. (F_Real,3)) * (<*uf*> @))
by MATRIX_0:def 7
.=
1
by A5, MATRIX_0:23
;
(Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 = uf . 2thus
(Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1
= uf . 2
verumproof
A12:
[2,1] in Indices ((1. (F_Real,3)) * (<*uf*> @))
by A5, MATRIX_0:23, Th2;
A13:
width (1. (F_Real,3)) = len (<*uf*> @)
by A3, MATRIX_0:23;
reconsider a1 = 1,
a2 =
0 as
Element of
F_Real ;
A14:
(
Line (
(1. (F_Real,3)),2)
= <*a2,a1,a2*> &
uf = <*(uf . 1),(uf . 2),(uf . 3)*> )
by Th56, A1, FINSEQ_1:45;
dom uf = Seg 3
by A1, FINSEQ_1:def 3;
then reconsider uf1 =
uf . 1,
uf2 =
uf . 2,
uf3 =
uf . 3 as
Element of
F_Real by FINSEQ_1:1, FINSEQ_2:11;
A15:
(Line ((1. (F_Real,3)),2)) "*" uf =
((a2 * uf1) + (a1 * uf2)) + (a2 * uf3)
by A14, Th6
.=
uf . 2
;
1
in Seg 1
by FINSEQ_1:1;
then
1
in Seg (width ((1. (F_Real,3)) * (<*uf*> @)))
by A5, MATRIX_0:23;
then (Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1 =
((1. (F_Real,3)) * (<*uf*> @)) * (2,1)
by MATRIX_0:def 7
.=
(Line ((1. (F_Real,3)),2)) "*" (Col ((<*uf*> @),1))
by A12, A13, MATRIX_3:def 4
.=
(Line ((1. (F_Real,3)),2)) "*" uf
by Th76
;
hence
(Line (((1. (F_Real,3)) * (<*uf*> @)),2)) . 1
= uf . 2
by A15;
verum
end; end;
hence
((1. (F_Real,3)) * (<*uf*> @)) . 2
= <*(uf . 2)*>
by A11, FINSEQ_1:40;
verum
end; thus
((1. (F_Real,3)) * (<*uf*> @)) . 3
= <*(uf . 3)*>
verumproof
3
in Seg 3
by FINSEQ_1:1;
then A16:
((1. (F_Real,3)) * (<*uf*> @)) . 3
= Line (
((1. (F_Real,3)) * (<*uf*> @)),3)
by A5, MATRIX_0:52;
now ( len (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) = 1 & (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = uf . 3 )thus len (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) =
width ((1. (F_Real,3)) * (<*uf*> @))
by MATRIX_0:def 7
.=
1
by A5, MATRIX_0:23
;
(Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 = uf . 3thus
(Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1
= uf . 3
verumproof
A17:
[3,1] in Indices ((1. (F_Real,3)) * (<*uf*> @))
by A5, MATRIX_0:23, Th2;
A18:
width (1. (F_Real,3)) = len (<*uf*> @)
by A3, MATRIX_0:23;
reconsider a1 = 1,
a2 =
0 as
Element of
F_Real ;
A19:
(
Line (
(1. (F_Real,3)),3)
= <*a2,a2,a1*> &
uf = <*(uf . 1),(uf . 2),(uf . 3)*> )
by Th56, A1, FINSEQ_1:45;
dom uf = Seg 3
by A1, FINSEQ_1:def 3;
then reconsider uf1 =
uf . 1,
uf2 =
uf . 2,
uf3 =
uf . 3 as
Element of
F_Real by FINSEQ_1:1, FINSEQ_2:11;
A20:
(Line ((1. (F_Real,3)),3)) "*" uf =
((a2 * uf1) + (a2 * uf2)) + (a1 * uf3)
by A19, Th6
.=
uf . 3
;
1
in Seg 1
by FINSEQ_1:1;
then
1
in Seg (width ((1. (F_Real,3)) * (<*uf*> @)))
by A5, MATRIX_0:23;
then (Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1 =
((1. (F_Real,3)) * (<*uf*> @)) * (3,1)
by MATRIX_0:def 7
.=
(Line ((1. (F_Real,3)),3)) "*" (Col ((<*uf*> @),1))
by A17, A18, MATRIX_3:def 4
.=
(Line ((1. (F_Real,3)),3)) "*" uf
by Th76
;
hence
(Line (((1. (F_Real,3)) * (<*uf*> @)),3)) . 1
= uf . 3
by A20;
verum
end; end;
hence
((1. (F_Real,3)) * (<*uf*> @)) . 3
= <*(uf . 3)*>
by A16, FINSEQ_1:40;
verum
end; end;
hence
<*uf*> @ = (1. (F_Real,3)) * (<*uf*> @)
by A2, FINSEQ_1:45; verum