let p, q, r be Point of (TOP-REAL 3); for PQR being Matrix of 3,F_Real st PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> holds
( Col (PQR,1) = <*(p `1),(q `1),(r `1)*> & Col (PQR,2) = <*(p `2),(q `2),(r `2)*> & Col (PQR,3) = <*(p `3),(q `3),(r `3)*> )
let PQR be Matrix of 3,F_Real; ( PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> implies ( Col (PQR,1) = <*(p `1),(q `1),(r `1)*> & Col (PQR,2) = <*(p `2),(q `2),(r `2)*> & Col (PQR,3) = <*(p `3),(q `3),(r `3)*> ) )
assume A1:
PQR = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*>
; ( Col (PQR,1) = <*(p `1),(q `1),(r `1)*> & Col (PQR,2) = <*(p `2),(q `2),(r `2)*> & Col (PQR,3) = <*(p `3),(q `3),(r `3)*> )
len PQR = 3
by MATRIX_0:24;
then A2:
dom PQR = Seg 3
by FINSEQ_1:def 3;
A3:
PQR = <*<*(PQR * (1,1)),(PQR * (1,2)),(PQR * (1,3))*>,<*(PQR * (2,1)),(PQR * (2,2)),(PQR * (2,3))*>,<*(PQR * (3,1)),(PQR * (3,2)),(PQR * (3,3))*>*>
by MATRIXR2:37;
then
PQR . 1 = <*(PQR * (1,1)),(PQR * (1,2)),(PQR * (1,3))*>
by FINSEQ_1:45;
then A4:
<*(PQR * (1,1)),(PQR * (1,2)),(PQR * (1,3))*> = <*(p `1),(p `2),(p `3)*>
by A1, FINSEQ_1:45;
PQR . 2 = <*(PQR * (2,1)),(PQR * (2,2)),(PQR * (2,3))*>
by A3, FINSEQ_1:45;
then A5:
<*(PQR * (2,1)),(PQR * (2,2)),(PQR * (2,3))*> = <*(q `1),(q `2),(q `3)*>
by A1, FINSEQ_1:45;
PQR . 3 = <*(PQR * (3,1)),(PQR * (3,2)),(PQR * (3,3))*>
by A3, FINSEQ_1:45;
then A6:
<*(PQR * (3,1)),(PQR * (3,2)),(PQR * (3,3))*> = <*(r `1),(r `2),(r `3)*>
by A1, FINSEQ_1:45;
now ( len (Col (PQR,1)) = 3 & len (Col (PQR,2)) = 3 & len (Col (PQR,3)) = 3 & (Col (PQR,1)) . 1 = p `1 & (Col (PQR,1)) . 2 = q `1 & (Col (PQR,1)) . 3 = r `1 & (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus len (Col (PQR,1)) =
len PQR
by MATRIX_0:def 8
.=
3
by MATRIX_0:24
;
( len (Col (PQR,2)) = 3 & len (Col (PQR,3)) = 3 & (Col (PQR,1)) . 1 = p `1 & (Col (PQR,1)) . 2 = q `1 & (Col (PQR,1)) . 3 = r `1 & (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus len (Col (PQR,2)) =
len PQR
by MATRIX_0:def 8
.=
3
by MATRIX_0:24
;
( len (Col (PQR,3)) = 3 & (Col (PQR,1)) . 1 = p `1 & (Col (PQR,1)) . 2 = q `1 & (Col (PQR,1)) . 3 = r `1 & (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus len (Col (PQR,3)) =
len PQR
by MATRIX_0:def 8
.=
3
by MATRIX_0:24
;
( (Col (PQR,1)) . 1 = p `1 & (Col (PQR,1)) . 2 = q `1 & (Col (PQR,1)) . 3 = r `1 & (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,1)) . 1 =
PQR * (1,1)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
p `1
by A4, FINSEQ_1:78
;
( (Col (PQR,1)) . 2 = q `1 & (Col (PQR,1)) . 3 = r `1 & (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,1)) . 2 =
PQR * (2,1)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
q `1
by A5, FINSEQ_1:78
;
( (Col (PQR,1)) . 3 = r `1 & (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,1)) . 3 =
PQR * (3,1)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
r `1
by A6, FINSEQ_1:78
;
( (Col (PQR,2)) . 1 = p `2 & (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,2)) . 1 =
PQR * (1,2)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
p `2
by A4, FINSEQ_1:78
;
( (Col (PQR,2)) . 2 = q `2 & (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,2)) . 2 =
PQR * (2,2)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
q `2
by A5, FINSEQ_1:78
;
( (Col (PQR,2)) . 3 = r `2 & (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,2)) . 3 =
PQR * (3,2)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
r `2
by A6, FINSEQ_1:78
;
( (Col (PQR,3)) . 1 = p `3 & (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,3)) . 1 =
PQR * (1,3)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
p `3
by A4, FINSEQ_1:78
;
( (Col (PQR,3)) . 2 = q `3 & (Col (PQR,3)) . 3 = r `3 )thus (Col (PQR,3)) . 2 =
PQR * (2,3)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
q `3
by A5, FINSEQ_1:78
;
(Col (PQR,3)) . 3 = r `3 thus (Col (PQR,3)) . 3 =
PQR * (3,3)
by A2, MATRIX_0:def 8, FINSEQ_1:1
.=
r `3
by A6, FINSEQ_1:78
;
verum end;
hence
( Col (PQR,1) = <*(p `1),(q `1),(r `1)*> & Col (PQR,2) = <*(p `2),(q `2),(r `2)*> & Col (PQR,3) = <*(p `3),(q `3),(r `3)*> )
by FINSEQ_1:45; verum