let NR, MR be Matrix of 3,REAL; :: thesis:
let p1, p2, p3 be FinSequence of REAL ; :: thesis:
assume that
A1: ( p1 = <*1,0,0*> & p2 = <*0,1,0*> & p3 = <*0,0,1*> ) and
A2: NR * p1 = MR * p1 and
A3: NR * p2 = MR * p2 and
A4: NR * p3 = MR * p3 ; :: thesis:
reconsider N = NR, M = MR as Matrix of 3,F_Real ;
consider n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real such that
A5: N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> by PASCAL:3;
consider m11, m12, m13, m21, m22, m23, m31, m32, m33 being Element of F_Real such that
A6: M = <*<*m11,m12,m13*>,<*m21,m22,m23*>,<*m31,m32,m33*>*> by PASCAL:3;
reconsider rn11 = n11, rn12 = n12, rn13 = n13, rn21 = n21, rn22 = n22, rn23 = n23, rn31 = n31, rn32 = n32, rn33 = n33 as Element of REAL ;
reconsider rm11 = m11, rm12 = m12, rm13 = m13, rm21 = m21, rm22 = m22, rm23 = m23, rm31 = m31, rm32 = m32, rm33 = m33 as Element of REAL ;
A7: |[1,0,0]| in TOP-REAL 3 ;
then reconsider q1 = <*1,0,0*> as FinSequence of REAL by EUCLID:24;
reconsider z1 = q1 . 1, z2 = q1 . 2, z3 = q1 . 3 as Element of REAL by XREAL_0:def 1;
A8: ( z1 = 1 & z2 = 0 & z3 = 0 ) by FINSEQ_1:45;
q1 in REAL 3 by A7, EUCLID:22;
then A9: len q1 = 3 by EUCLID_8:50;
then ( NR = <*<*rn11,rn12,rn13*>,<*rn21,rn22,rn23*>,<*rn31,rn32,rn33*>*> & q1 = <*z1,z2,z3*> ) by FINSEQ_1:45, A5;
then A10: NR * q1 = <*(((rn11 * z1) + (rn12 * z2)) + (rn13 * z3)),(((rn21 * z1) + (rn22 * z2)) + (rn23 * z3)),(((rn31 * z1) + (rn32 * z2)) + (rn33 * z3))*> by PASCAL:9
.= <*rn11,rn21,rn31*> by A8 ;
( MR = <*<*rm11,rm12,rm13*>,<*rm21,rm22,rm23*>,<*rm31,rm32,rm33*>*> & q1 = <*z1,z2,z3*> ) by A9, FINSEQ_1:45, A6;
then MR * q1 = <*(((rm11 * z1) + (rm12 * z2)) + (rm13 * z3)),(((rm21 * z1) + (rm22 * z2)) + (rm23 * z3)),(((rm31 * z1) + (rm32 * z2)) + (rm33 * z3))*> by PASCAL:9
.= <*rm11,rm21,rm31*> by A8 ;
then A11: ( rn11 = rm11 & rn21 = rm21 & rn31 = rm31 ) by A10, A2, A1, FINSEQ_1:78;
A12: |[0,1,0]| in TOP-REAL 3 ;
then reconsider q1 = <*0,1,0*> as FinSequence of REAL by EUCLID:24;
reconsider z1 = q1 . 1, z2 = q1 . 2, z3 = q1 . 3 as Element of REAL by XREAL_0:def 1;
A13: ( z1 = 0 & z2 = 1 & z3 = 0 ) by FINSEQ_1:45;
q1 in REAL 3 by A12, EUCLID:22;
then A14: len q1 = 3 by EUCLID_8:50;
then ( NR = <*<*rn11,rn12,rn13*>,<*rn21,rn22,rn23*>,<*rn31,rn32,rn33*>*> & q1 = <*z1,z2,z3*> ) by FINSEQ_1:45, A5;
then A15: NR * q1 = <*(((rn11 * z1) + (rn12 * z2)) + (rn13 * z3)),(((rn21 * z1) + (rn22 * z2)) + (rn23 * z3)),(((rn31 * z1) + (rn32 * z2)) + (rn33 * z3))*> by PASCAL:9
.= <*rn12,rn22,rn32*> by A13 ;
( MR = <*<*rm11,rm12,rm13*>,<*rm21,rm22,rm23*>,<*rm31,rm32,rm33*>*> & q1 = <*z1,z2,z3*> ) by A14, FINSEQ_1:45, A6;
then MR * q1 = <*(((rm11 * z1) + (rm12 * z2)) + (rm13 * z3)),(((rm21 * z1) + (rm22 * z2)) + (rm23 * z3)),(((rm31 * z1) + (rm32 * z2)) + (rm33 * z3))*> by PASCAL:9
.= <*rm12,rm22,rm32*> by A13 ;
then A16: ( rn12 = rm12 & rn22 = rm22 & rn32 = rm32 ) by A15, A3, A1, FINSEQ_1:78;
A17: |[0,0,1]| in TOP-REAL 3 ;
then reconsider q1 = <*0,0,1*> as FinSequence of REAL by EUCLID:24;
reconsider z1 = q1 . 1, z2 = q1 . 2, z3 = q1 . 3 as Element of REAL by XREAL_0:def 1;
A18: ( z1 = 0 & z2 = 0 & z3 = 1 ) by FINSEQ_1:45;
q1 in REAL 3 by A17, EUCLID:22;
then A19: len q1 = 3 by EUCLID_8:50;
then ( NR = <*<*rn11,rn12,rn13*>,<*rn21,rn22,rn23*>,<*rn31,rn32,rn33*>*> & q1 = <*z1,z2,z3*> ) by FINSEQ_1:45, A5;
then A20: NR * q1 = <*(((rn11 * z1) + (rn12 * z2)) + (rn13 * z3)),(((rn21 * z1) + (rn22 * z2)) + (rn23 * z3)),(((rn31 * z1) + (rn32 * z2)) + (rn33 * z3))*> by PASCAL:9
.= <*rn13,rn23,rn33*> by A18 ;
( MR = <*<*rm11,rm12,rm13*>,<*rm21,rm22,rm23*>,<*rm31,rm32,rm33*>*> & q1 = <*z1,z2,z3*> ) by A19, FINSEQ_1:45, A6;
then MR * q1 = <*(((rm11 * z1) + (rm12 * z2)) + (rm13 * z3)),(((rm21 * z1) + (rm22 * z2)) + (rm23 * z3)),(((rm31 * z1) + (rm32 * z2)) + (rm33 * z3))*> by PASCAL:9
.= <*rm13,rm23,rm33*> by A18 ;
then ( rn13 = rm13 & rn23 = rm23 & rn33 = rm33 ) by A20, A4, A1, FINSEQ_1:78;
hence NR = MR by A11, A16, A5, A6; :: thesis: