let p, q, r be Point of (TOP-REAL 3); :: thesis: 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; :: thesis: ( 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)*>*> ; :: thesis: ( 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 :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: ( (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 ; :: thesis: (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 ; :: thesis: 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; :: thesis: verum