let a, b be Element of F_Real; :: thesis: for p being FinSequence of REAL
for M being Matrix of 3,REAL st len p = 3 holds
|((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|
let p be FinSequence of REAL ; :: thesis: for M being Matrix of 3,REAL st len p = 3 holds
|((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|
let M be Matrix of 3,REAL; :: thesis: ( len p = 3 implies |((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))| )
assume A1: len p = 3 ; :: thesis: |((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))|
A2: ( width M = 3 & len M = 3 ) by MATRIX_0:23;
A3: len (b * p) = 3 by A1, RVSUM_1:117;
A4: p is Element of REAL 3 by A1, EUCLID_8:2;
A5: p * M = Line (((LineVec2Mx p) * M),1) by MATRIXR1:def 12;
A6: width (MXR2MXF (LineVec2Mx p)) = width (LineVec2Mx p) by MATRIXR1:def 1
.= len p by MATRIXR1:def 10
.= len (MXR2MXF M) by A1, MATRIX_0:23 ;
(LineVec2Mx p) * M = MXF2MXR ((MXR2MXF (LineVec2Mx p)) * (MXR2MXF M)) by MATRIXR1:def 6
.= (MXR2MXF (LineVec2Mx p)) * (MXR2MXF M) by MATRIXR1:def 2 ;
then width ((LineVec2Mx p) * M) = width (MXR2MXF M) by A6, MATRIX_3:def 4
.= width M by MATRIXR1:def 1 ;
then len (Line (((LineVec2Mx p) * M),1)) = width M by MATRIX_0:def 7;
then A7: p * M is Element of REAL 3 by A5, MATRIX_0:23, EUCLID_8:2;
len (b * p) > 0 by A1, RVSUM_1:117;
then A8: len (ColVec2Mx (b * p)) = len (b * p) by MATRIXR1:def 9
.= 3 by A1, RVSUM_1:117 ;
A9: width (MXR2MXF M) = 3 by MATRIX_0:23
.= len (MXR2MXF (ColVec2Mx (b * p))) by A8, MATRIXR1:def 1 ;
len (M * (b * p)) = len (Col ((M * (ColVec2Mx (b * p))),1)) by MATRIXR1:def 11
.= len (M * (ColVec2Mx (b * p))) by MATRIX_0:def 8
.= len (MXF2MXR ((MXR2MXF M) * (MXR2MXF (ColVec2Mx (b * p))))) by MATRIXR1:def 6
.= len ((MXR2MXF M) * (MXR2MXF (ColVec2Mx (b * p)))) by MATRIXR1:def 2
.= len (MXR2MXF M) by A9, MATRIX_3:def 4
.= 3 by MATRIX_0:23 ;
then M * (b * p) is Element of REAL 3 by EUCLID_8:2;
then |((a * p),(M * (b * p)))| = a * |((M * (b * p)),p)| by A4, EUCLID_4:21
.= a * |((p * M),(b * p))| by MATRPROB:47, A2, A3, A1
.= a * (b * |(p,(p * M))|) by EUCLID_4:21, A4, A7
.= (a * b) * |((p * M),p)|
.= (a * b) * |((M * p),p)| by A2, A1, MATRPROB:47 ;
hence |((a * p),(M * (b * p)))| = (a * b) * |(p,(M * p))| ; :: thesis: verum