let p be FinSequence of REAL ; for M being Matrix of 3,REAL
for a, b, c, d, e, f, g, h, i, p1, p2, p3 being Element of REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & p = <*p1,p2,p3*> holds
M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>
let M be Matrix of 3,REAL; for a, b, c, d, e, f, g, h, i, p1, p2, p3 being Element of REAL st M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & p = <*p1,p2,p3*> holds
M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>
let a, b, c, d, e, f, g, h, i, p1, p2, p3 be Element of REAL ; ( M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*> & p = <*p1,p2,p3*> implies M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*> )
assume that
A1:
M = <*<*a,b,c*>,<*d,e,f*>,<*g,h,i*>*>
and
A2:
p = <*p1,p2,p3*>
; M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>
A3:
( p . 1 = p1 & p . 2 = p2 & p . 3 = p3 )
by A2, FINSEQ_1:45;
p = |[p1,p2,p3]|
by A2;
then reconsider ru = p as Element of REAL 3 by EUCLID:22;
A4:
MXR2MXF (ColVec2Mx p) = <*ru*> @
by ANPROJ_8:72;
reconsider a = a, b = b, c = c, d = d, e = e, f = f, g = g, h = h, i = i as Element of F_Real ;
reconsider fu1 = ru . 1, fu2 = ru . 2, fu3 = ru . 3 as Element of F_Real by XREAL_0:def 1;
A5:
<*ru*> @ = <*<*fu1*>,<*fu2*>,<*fu3*>*>
by EUCLID_8:50, ANPROJ_8:77;
A6:
len ru = 3
by EUCLID_8:50;
A7:
len <*ru*> = 1
by FINSEQ_1:39;
rng <*ru*> = {ru}
by FINSEQ_1:39;
then
ru in rng <*ru*>
by TARSKI:def 1;
then A8:
width <*ru*> = 3
by A6, A7, MATRIX_0:def 3;
then A9: width (<*ru*> @) =
len <*ru*>
by MATRIX_0:29
.=
1
by FINSEQ_1:39
;
A10:
len (<*ru*> @) = 3
by MATRIX_0:def 6, A8;
then A11:
<*ru*> @ is Matrix of 3,1,F_Real
by A9, MATRIX_0:20;
reconsider M2 = <*ru*> @ as Matrix of 3,1,F_Real by A10, A9, MATRIX_0:20;
A12: M * (ColVec2Mx p) =
M * (<*ru*> @)
by A4, MATRIXR1:def 1
.=
MXF2MXR ((MXR2MXF M) * (MXR2MXF (<*ru*> @)))
by MATRIXR1:def 6
;
A13:
MXR2MXF (<*ru*> @) is Matrix of 3,1,F_Real
by MATRIXR1:def 1, A11;
A14:
MXR2MXF (<*ru*> @) = <*<*fu1*>,<*fu2*>,<*fu3*>*>
by A5, MATRIXR1:def 1;
A15:
(MXR2MXF M) * (MXR2MXF (<*ru*> @)) = <*<*(((a * fu1) + (b * fu2)) + (c * fu3))*>,<*(((d * fu1) + (e * fu2)) + (f * fu3))*>,<*(((g * fu1) + (h * fu2)) + (i * fu3))*>*>
by A13, A1, MATRIXR1:def 1, A14, ANPROJ_9:7;
reconsider q = <*(((a * fu1) + (b * fu2)) + (c * fu3)),(((d * fu1) + (e * fu2)) + (f * fu3)),(((g * fu1) + (h * fu2)) + (i * fu3))*> as FinSequence of REAL ;
A16:
( q . 1 = ((a * fu1) + (b * fu2)) + (c * fu3) & q . 2 = ((d * fu1) + (e * fu2)) + (f * fu3) & q . 3 = ((g * fu1) + (h * fu2)) + (i * fu3) )
by FINSEQ_1:45;
q = |[(((a * fu1) + (b * fu2)) + (c * fu3)),(((d * fu1) + (e * fu2)) + (f * fu3)),(((g * fu1) + (h * fu2)) + (i * fu3))]|
;
then reconsider rq = q as Element of REAL 3 by EUCLID:22;
reconsider qf = q as FinSequence of F_Real ;
A17:
len q = 3
by FINSEQ_1:45;
A18: ColVec2Mx rq =
MXR2MXF (ColVec2Mx rq)
by MATRIXR1:def 1
.=
<*qf*> @
by ANPROJ_8:72
;
then A19: ColVec2Mx rq =
F2M q
by A17, ANPROJ_8:88
.=
<*<*(((a * fu1) + (b * fu2)) + (c * fu3))*>,<*(((d * fu1) + (e * fu2)) + (f * fu3))*>,<*(((g * fu1) + (h * fu2)) + (i * fu3))*>*>
by A16, A17, ANPROJ_8:def 1
.=
M * (ColVec2Mx p)
by A15, A12, MATRIXR1:def 2
;
M * p =
Col ((ColVec2Mx rq),1)
by A19, MATRIXR1:def 11
.=
<*(((a * fu1) + (b * fu2)) + (c * fu3)),(((d * fu1) + (e * fu2)) + (f * fu3)),(((g * fu1) + (h * fu2)) + (i * fu3))*>
by A18, ANPROJ_8:93
;
hence
M * p = <*(((a * p1) + (b * p2)) + (c * p3)),(((d * p1) + (e * p2)) + (f * p3)),(((g * p1) + (h * p2)) + (i * p3))*>
by A3; verum