let p, q, r be Point of (TOP-REAL 3); :: thesis: for M, PQR being Matrix of 3,F_Real
for pf, qf, rf being FinSequence of F_Real
for pt, qt, rt being FinSequence of 1 -tuples_on REAL st PQR = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf holds
(M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*>
let M, PQR be Matrix of 3,F_Real; :: thesis: for pf, qf, rf being FinSequence of F_Real
for pt, qt, rt being FinSequence of 1 -tuples_on REAL st PQR = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf holds
(M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*>
let pf, qf, rf be FinSequence of F_Real; :: thesis: for pt, qt, rt being FinSequence of 1 -tuples_on REAL st PQR = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf holds
(M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*>
let pt, qt, rt be FinSequence of 1 -tuples_on REAL; :: thesis: ( PQR = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> & p = pf & q = qf & r = rf & pt = M * pf & qt = M * qf & rt = M * rf implies (M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*> )
assume that
A1: PQR = <*<*(p `1),(q `1),(r `1)*>,<*(p `2),(q `2),(r `2)*>,<*(p `3),(q `3),(r `3)*>*> and
A2: p = pf and
A3: q = qf and
A4: r = rf and
A5: pt = M * pf and
A6: qt = M * qf and
A7: rt = M * rf ; :: thesis: (M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*>
A8: PQR @ = <*<*(p `1),(p `2),(p `3)*>,<*(q `1),(q `2),(q `3)*>,<*(r `1),(r `2),(r `3)*>*> by A1, Th19;
A9: len PQR = 3 by MATRIX_0:24;
A10: width PQR = 3 by MATRIX_0:23;
A11: Indices (M * PQR) = [:(Seg 3),(Seg 3):] by MATRIX_0:24;
len (PQR @) = 3 by MATRIX_0:23;
then A12: dom (PQR @) = Seg 3 by FINSEQ_1:def 3;
then A13: Col (((PQR @) @),1) = Line ((PQR @),1) by FINSEQ_1:1, MATRIX_0:58
.= p by A8, Th60 ;
A14: Col (((PQR @) @),2) = Line ((PQR @),2) by A12, FINSEQ_1:1, MATRIX_0:58
.= q by A8, Th60 ;
A15: Col (((PQR @) @),3) = Line ((PQR @),3) by A12, FINSEQ_1:1, MATRIX_0:58
.= r by A8, Th60 ;
( pf in TOP-REAL 3 & qf in TOP-REAL 3 & rf in TOP-REAL 3 ) by A2, A3, A4;
then A16: ( pf in REAL 3 & qf in REAL 3 & rf in REAL 3 ) by EUCLID:22;
then A17: ( len pf = 3 & len qf = 3 & len rf = 3 ) by EUCLID_8:50;
A18: ( width M = len (<*pf*> @) & width M = len (<*qf*> @) & width M = len (<*rf*> @) )
proof
width <*pf*> = 3 by A17, Th61;
then len (<*pf*> @) = width <*pf*> by MATRIX_0:29
.= len pf by MATRIX_0:23 ;
then len (<*pf*> @) = 3 by A16, EUCLID_8:50;
hence width M = len (<*pf*> @) by MATRIX_0:23; :: thesis: ( width M = len (<*qf*> @) & width M = len (<*rf*> @) )
width <*qf*> = 3 by A17, Th61;
then len (<*qf*> @) = width <*qf*> by MATRIX_0:29
.= len qf by MATRIX_0:23 ;
then len (<*qf*> @) = 3 by A16, EUCLID_8:50;
hence width M = len (<*qf*> @) by MATRIX_0:23; :: thesis: width M = len (<*rf*> @)
width <*rf*> = 3 by A17, Th61;
then len (<*rf*> @) = width <*rf*> by MATRIX_0:29
.= len rf by MATRIX_0:23 ;
then len (<*rf*> @) = 3 by A16, EUCLID_8:50;
hence width M = len (<*rf*> @) by MATRIX_0:23; :: thesis: verum
end;
A19: ( len pt = 3 & len qt = 3 & len rt = 3 )
proof
( width M = len (<*pf*> @) & len M = 3 ) by MATRIX_0:23, A18;
then len (M * (<*pf*> @)) = 3 by MATRIX_3:def 4;
hence len pt = 3 by A5, LAPLACE:def 9; :: thesis: ( len qt = 3 & len rt = 3 )
( width M = len (<*qf*> @) & len M = 3 ) by A18, MATRIX_0:23;
then len (M * (<*qf*> @)) = 3 by MATRIX_3:def 4;
hence len qt = 3 by A6, LAPLACE:def 9; :: thesis: len rt = 3
( width M = len (<*rf*> @) & len M = 3 ) by A18, MATRIX_0:23;
then len (M * (<*rf*> @)) = 3 by MATRIX_3:def 4;
hence len rt = 3 by A7, LAPLACE:def 9; :: thesis: verum
end;
set PQRM = <*<*(pt . 1),(pt . 2),(pt . 3)*>,<*(qt . 1),(qt . 2),(qt . 3)*>,<*(rt . 1),(rt . 2),(rt . 3)*>*>;
A20: dom (M * PQR) = Seg (len (M * PQR)) by FINSEQ_1:def 3
.= Seg 3 by MATRIX_0:24 ;
A21: width (M * PQR) = 3 by MATRIX_0:23;
A22: len ((M * PQR) @) = 3 by MATRIX_0:23;
then A23: dom ((M * PQR) @) = Seg 3 by FINSEQ_1:def 3;
A24: ( 1 in Seg (width (M * PQR)) & 2 in Seg (width (M * PQR)) & 3 in Seg (width (M * PQR)) ) by A21, FINSEQ_1:1;
now :: thesis: ( dom ((M * PQR) @) = dom <*(M2F pt),(M2F qt),(M2F rt)*> & ( for x being object st x in dom ((M * PQR) @) holds
((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x ) )
len <*(M2F pt),(M2F qt),(M2F rt)*> = 3 by FINSEQ_1:45;
hence dom ((M * PQR) @) = dom <*(M2F pt),(M2F qt),(M2F rt)*> by A23, FINSEQ_1:def 3; :: thesis: for x being object st x in dom ((M * PQR) @) holds
((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x
thus for x being object st x in dom ((M * PQR) @) holds
((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x :: thesis: verum
proof
let x be object ; :: thesis: ( x in dom ((M * PQR) @) implies ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x )
assume A25: x in dom ((M * PQR) @) ; :: thesis: ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x
then reconsider y = x as Nat ;
y in Seg 3 by A25, A22, FINSEQ_1:def 3;
then not not y = 1 & ... & not y = 3 by FINSEQ_1:91;
per cases then ( y = 1 or y = 2 or y = 3 ) ;
suppose A26: y = 1 ; :: thesis: ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x
A27: M * (<*pf*> @) is Matrix of 3,1,F_Real by A16, EUCLID_8:50, Th74;
then A28: Indices (M * (<*pf*> @)) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
A29: now :: thesis: ( len pt = 3 & <*((Line ((M * PQR),1)) . 1)*> = pt . 1 & <*((Line ((M * PQR),2)) . 1)*> = pt . 2 & <*((Line ((M * PQR),3)) . 1)*> = pt . 3 )
thus len pt = 3 by A19; :: thesis: ( <*((Line ((M * PQR),1)) . 1)*> = pt . 1 & <*((Line ((M * PQR),2)) . 1)*> = pt . 2 & <*((Line ((M * PQR),3)) . 1)*> = pt . 3 )
<*((M * PQR) * (1,1))*> = pt . 1
proof
1 in Seg 3 by FINSEQ_1:1;
then A30: ( width M = len PQR & [1,1] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A31: (M * (<*pf*> @)) . 1 = <*((Line (M,1)) "*" (Col (PQR,1)))*>
proof
A32: 1 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*pf*> @)),1) = <*((Line (M,1)) "*" (Col (PQR,1)))*>
proof
( 1 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A33: [1,1] in Indices (M * (<*pf*> @)) by A28, ZFMISC_1:87;
len pf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*pf*> @)),1) = <*((M * (<*pf*> @)) * (1,1))*> by Th75
.= <*((Line (M,1)) "*" (Col ((<*pf*> @),1)))*> by A18, A33, MATRIX_3:def 4
.= <*((Line (M,1)) "*" pf)*> by Th76
.= <*((Line (M,1)) "*" (Col (PQR,1)))*> by A13, A9, A10, MATRIX_0:57, A2 ;
hence Line ((M * (<*pf*> @)),1) = <*((Line (M,1)) "*" (Col (PQR,1)))*> ; :: thesis: verum
end;
hence (M * (<*pf*> @)) . 1 = <*((Line (M,1)) "*" (Col (PQR,1)))*> by A32, A27, MATRIX_0:52; :: thesis: verum
end;
pt . 1 = (M * (<*pf*> @)) . 1 by A5, LAPLACE:def 9;
hence <*((M * PQR) * (1,1))*> = pt . 1 by A30, MATRIX_3:def 4, A31; :: thesis: verum
end;
hence <*((Line ((M * PQR),1)) . 1)*> = pt . 1 by A24, MATRIX_0:def 7; :: thesis: ( <*((Line ((M * PQR),2)) . 1)*> = pt . 2 & <*((Line ((M * PQR),3)) . 1)*> = pt . 3 )
<*((M * PQR) * (2,1))*> = pt . 2
proof
( 1 in Seg 3 & 2 in Seg 3 ) by FINSEQ_1:1;
then A34: ( width M = len PQR & [2,1] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A34BIS: (M * (<*pf*> @)) . 2 = <*((Line (M,2)) "*" (Col (PQR,1)))*>
proof
A35: 2 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*pf*> @)),2) = <*((Line (M,2)) "*" (Col (PQR,1)))*>
proof
( 1 in Seg 1 & 2 in Seg 3 ) by FINSEQ_1:1;
then A36: [2,1] in Indices (M * (<*pf*> @)) by A28, ZFMISC_1:87;
len pf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*pf*> @)),2) = <*((M * (<*pf*> @)) * (2,1))*> by Th75
.= <*((Line (M,2)) "*" (Col ((<*pf*> @),1)))*> by A18, A36, MATRIX_3:def 4
.= <*((Line (M,2)) "*" pf)*> by Th76
.= <*((Line (M,2)) "*" (Col (PQR,1)))*> by A13, A9, A10, MATRIX_0:57, A2 ;
hence Line ((M * (<*pf*> @)),2) = <*((Line (M,2)) "*" (Col (PQR,1)))*> ; :: thesis: verum
end;
hence (M * (<*pf*> @)) . 2 = <*((Line (M,2)) "*" (Col (PQR,1)))*> by A35, A27, MATRIX_0:52; :: thesis: verum
end;
pt . 2 = (M * (<*pf*> @)) . 2 by A5, LAPLACE:def 9;
hence <*((M * PQR) * (2,1))*> = pt . 2 by A34, MATRIX_3:def 4, A34BIS; :: thesis: verum
end;
hence <*((Line ((M * PQR),2)) . 1)*> = pt . 2 by A24, MATRIX_0:def 7; :: thesis: <*((Line ((M * PQR),3)) . 1)*> = pt . 3
<*((M * PQR) * (3,1))*> = pt . 3
proof
( 1 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then A37: ( width M = len PQR & [3,1] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A38: (M * (<*pf*> @)) . 3 = <*((Line (M,3)) "*" (Col (PQR,1)))*>
proof
A39: 3 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*pf*> @)),3) = <*((Line (M,3)) "*" (Col (PQR,1)))*>
proof
( 1 in Seg 1 & 3 in Seg 3 ) by FINSEQ_1:1;
then A39BIS: [3,1] in Indices (M * (<*pf*> @)) by A28, ZFMISC_1:87;
len pf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*pf*> @)),3) = <*((M * (<*pf*> @)) * (3,1))*> by Th75
.= <*((Line (M,3)) "*" (Col ((<*pf*> @),1)))*> by A18, A39BIS, MATRIX_3:def 4
.= <*((Line (M,3)) "*" pf)*> by Th76
.= <*((Line (M,3)) "*" (Col (PQR,1)))*> by A13, A9, A10, MATRIX_0:57, A2 ;
hence Line ((M * (<*pf*> @)),3) = <*((Line (M,3)) "*" (Col (PQR,1)))*> ; :: thesis: verum
end;
hence (M * (<*pf*> @)) . 3 = <*((Line (M,3)) "*" (Col (PQR,1)))*> by A39, A27, MATRIX_0:52; :: thesis: verum
end;
pt . 3 = (M * (<*pf*> @)) . 3 by A5, LAPLACE:def 9;
hence <*((M * PQR) * (3,1))*> = pt . 3 by A37, MATRIX_3:def 4, A38; :: thesis: verum
end;
hence <*((Line ((M * PQR),3)) . 1)*> = pt . 3 by A24, MATRIX_0:def 7; :: thesis: verum
end;
A40: ( (Line ((M * PQR),1)) . 1 = (M * PQR) * (1,1) & (Line ((M * PQR),2)) . 1 = (M * PQR) * (2,1) & (Line ((M * PQR),3)) . 1 = (M * PQR) * (3,1) ) by A24, MATRIX_0:def 7;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then ( [1,1] in Indices (M * PQR) & [2,1] in Indices (M * PQR) & [3,1] in Indices (M * PQR) ) by A11, ZFMISC_1:87;
then A41: ( ((M * PQR) @) * (1,1) = (M * PQR) * (1,1) & ((M * PQR) @) * (1,2) = (M * PQR) * (2,1) & ((M * PQR) @) * (1,3) = (M * PQR) * (3,1) ) by MATRIX_0:def 6;
width ((M * PQR) @) = len (M * PQR) by A21, MATRIX_0:29;
then Seg (width ((M * PQR) @)) = dom (M * PQR) by FINSEQ_1:def 3;
then A43: ( (Line (((M * PQR) @),1)) . 1 = ((M * PQR) @) * (1,1) & (Line (((M * PQR) @),1)) . 2 = ((M * PQR) @) * (1,2) & (Line (((M * PQR) @),1)) . 3 = ((M * PQR) @) * (1,3) ) by A20, FINSEQ_1:1, MATRIX_0:def 7;
A44: 1 in Seg 3 by FINSEQ_1:1;
reconsider FMPQR = Line (((M * PQR) @),1) as FinSequence of REAL ;
width ((M * PQR) @) = 3 by MATRIX_0:23;
then A45: len FMPQR = 3 by MATRIX_0:def 7;
A46: <*<*((Line (((M * PQR) @),1)) . 1)*>,<*((Line (((M * PQR) @),1)) . 2)*>,<*((Line (((M * PQR) @),1)) . 3)*>*> = F2M FMPQR by A45, DEF1;
FMPQR = M2F (F2M FMPQR) by A45, Th70
.= M2F pt by A46, A43, A41, A29, FINSEQ_1:45, A40 ;
then ((M * PQR) @) . 1 = M2F pt by A44, MATRIX_0:52;
hence ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x by A26, FINSEQ_1:45; :: thesis: verum
end;
suppose A47: y = 2 ; :: thesis: ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x
A48: M * (<*qf*> @) is Matrix of 3,1,F_Real by A16, EUCLID_8:50, Th74;
then A49: Indices (M * (<*qf*> @)) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
A50: now :: thesis: ( len qt = 3 & <*((Line ((M * PQR),1)) . 2)*> = qt . 1 & <*((Line ((M * PQR),2)) . 2)*> = qt . 2 & <*((Line ((M * PQR),3)) . 2)*> = qt . 3 )
thus len qt = 3 by A19; :: thesis: ( <*((Line ((M * PQR),1)) . 2)*> = qt . 1 & <*((Line ((M * PQR),2)) . 2)*> = qt . 2 & <*((Line ((M * PQR),3)) . 2)*> = qt . 3 )
<*((M * PQR) * (1,2))*> = qt . 1
proof
( 1 in Seg 3 & 2 in Seg 3 ) by FINSEQ_1:1;
then A51: ( width M = len PQR & [1,2] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A52: (M * (<*qf*> @)) . 1 = <*((Line (M,1)) "*" (Col (PQR,2)))*>
proof
A53: 1 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*qf*> @)),1) = <*((Line (M,1)) "*" (Col (PQR,2)))*>
proof
( 1 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A54: [1,1] in Indices (M * (<*qf*> @)) by A49, ZFMISC_1:87;
len qf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*qf*> @)),1) = <*((M * (<*qf*> @)) * (1,1))*> by Th75
.= <*((Line (M,1)) "*" (Col ((<*qf*> @),1)))*> by A18, A54, MATRIX_3:def 4
.= <*((Line (M,1)) "*" qf)*> by Th76
.= <*((Line (M,1)) "*" (Col (PQR,2)))*> by A14, A9, A10, MATRIX_0:57, A3 ;
hence Line ((M * (<*qf*> @)),1) = <*((Line (M,1)) "*" (Col (PQR,2)))*> ; :: thesis: verum
end;
hence (M * (<*qf*> @)) . 1 = <*((Line (M,1)) "*" (Col (PQR,2)))*> by A53, A48, MATRIX_0:52; :: thesis: verum
end;
qt . 1 = (M * (<*qf*> @)) . 1 by A6, LAPLACE:def 9;
hence <*((M * PQR) * (1,2))*> = qt . 1 by A51, MATRIX_3:def 4, A52; :: thesis: verum
end;
hence <*((Line ((M * PQR),1)) . 2)*> = qt . 1 by A24, MATRIX_0:def 7; :: thesis: ( <*((Line ((M * PQR),2)) . 2)*> = qt . 2 & <*((Line ((M * PQR),3)) . 2)*> = qt . 3 )
<*((M * PQR) * (2,2))*> = qt . 2
proof
( 1 in Seg 3 & 2 in Seg 3 ) by FINSEQ_1:1;
then A55: ( width M = len PQR & [2,2] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A56: (M * (<*qf*> @)) . 2 = <*((Line (M,2)) "*" (Col (PQR,2)))*>
proof
A57: 2 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*qf*> @)),2) = <*((Line (M,2)) "*" (Col (PQR,2)))*>
proof
( 1 in Seg 1 & 2 in Seg 3 ) by FINSEQ_1:1;
then A58: [2,1] in Indices (M * (<*qf*> @)) by A49, ZFMISC_1:87;
len qf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*qf*> @)),2) = <*((M * (<*qf*> @)) * (2,1))*> by Th75
.= <*((Line (M,2)) "*" (Col ((<*qf*> @),1)))*> by A18, A58, MATRIX_3:def 4
.= <*((Line (M,2)) "*" qf)*> by Th76
.= <*((Line (M,2)) "*" (Col (PQR,2)))*> by A14, A9, A10, MATRIX_0:57, A3 ;
hence Line ((M * (<*qf*> @)),2) = <*((Line (M,2)) "*" (Col (PQR,2)))*> ; :: thesis: verum
end;
hence (M * (<*qf*> @)) . 2 = <*((Line (M,2)) "*" (Col (PQR,2)))*> by A57, A48, MATRIX_0:52; :: thesis: verum
end;
qt . 2 = (M * (<*qf*> @)) . 2 by A6, LAPLACE:def 9;
hence <*((M * PQR) * (2,2))*> = qt . 2 by A55, MATRIX_3:def 4, A56; :: thesis: verum
end;
hence <*((Line ((M * PQR),2)) . 2)*> = qt . 2 by A24, MATRIX_0:def 7; :: thesis: <*((Line ((M * PQR),3)) . 2)*> = qt . 3
<*((M * PQR) * (3,2))*> = qt . 3
proof
( 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then A57: ( width M = len PQR & [3,2] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A58: (M * (<*qf*> @)) . 3 = <*((Line (M,3)) "*" (Col (PQR,2)))*>
proof
A59: 3 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*qf*> @)),3) = <*((Line (M,3)) "*" (Col (PQR,2)))*>
proof
( 1 in Seg 1 & 3 in Seg 3 ) by FINSEQ_1:1;
then A59BIS: [3,1] in Indices (M * (<*qf*> @)) by A49, ZFMISC_1:87;
len qf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*qf*> @)),3) = <*((M * (<*qf*> @)) * (3,1))*> by Th75
.= <*((Line (M,3)) "*" (Col ((<*qf*> @),1)))*> by A18, A59BIS, MATRIX_3:def 4
.= <*((Line (M,3)) "*" qf)*> by Th76
.= <*((Line (M,3)) "*" (Col (PQR,2)))*> by A14, A9, A10, MATRIX_0:57, A3 ;
hence Line ((M * (<*qf*> @)),3) = <*((Line (M,3)) "*" (Col (PQR,2)))*> ; :: thesis: verum
end;
hence (M * (<*qf*> @)) . 3 = <*((Line (M,3)) "*" (Col (PQR,2)))*> by A59, A48, MATRIX_0:52; :: thesis: verum
end;
qt . 3 = (M * (<*qf*> @)) . 3 by A6, LAPLACE:def 9;
hence <*((M * PQR) * (3,2))*> = qt . 3 by A57, MATRIX_3:def 4, A58; :: thesis: verum
end;
hence <*((Line ((M * PQR),3)) . 2)*> = qt . 3 by A24, MATRIX_0:def 7; :: thesis: verum
end;
A60: ( (Line ((M * PQR),1)) . 2 = (M * PQR) * (1,2) & (Line ((M * PQR),2)) . 2 = (M * PQR) * (2,2) & (Line ((M * PQR),3)) . 2 = (M * PQR) * (3,2) ) by A24, MATRIX_0:def 7;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then ( [1,2] in Indices (M * PQR) & [2,2] in Indices (M * PQR) & [3,2] in Indices (M * PQR) ) by A11, ZFMISC_1:87;
then A61: ( ((M * PQR) @) * (2,1) = (M * PQR) * (1,2) & ((M * PQR) @) * (2,2) = (M * PQR) * (2,2) & ((M * PQR) @) * (2,3) = (M * PQR) * (3,2) ) by MATRIX_0:def 6;
width ((M * PQR) @) = len (M * PQR) by A21, MATRIX_0:29;
then Seg (width ((M * PQR) @)) = dom (M * PQR) by FINSEQ_1:def 3;
then A62: ( (Line (((M * PQR) @),2)) . 1 = ((M * PQR) @) * (2,1) & (Line (((M * PQR) @),2)) . 2 = ((M * PQR) @) * (2,2) & (Line (((M * PQR) @),2)) . 3 = ((M * PQR) @) * (2,3) ) by A20, FINSEQ_1:1, MATRIX_0:def 7;
A63: 2 in Seg 3 by FINSEQ_1:1;
reconsider FMPQR = Line (((M * PQR) @),2) as FinSequence of REAL ;
width ((M * PQR) @) = 3 by MATRIX_0:23;
then A64: len FMPQR = 3 by MATRIX_0:def 7;
then A65: <*<*((Line (((M * PQR) @),2)) . 1)*>,<*((Line (((M * PQR) @),2)) . 2)*>,<*((Line (((M * PQR) @),2)) . 3)*>*> = F2M FMPQR by DEF1;
FMPQR = M2F (F2M FMPQR) by A64, Th70
.= M2F qt by A65, A62, A61, A50, FINSEQ_1:45, A60 ;
then ((M * PQR) @) . 2 = M2F qt by A63, MATRIX_0:52;
hence ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x by A47, FINSEQ_1:45; :: thesis: verum
end;
suppose A66: y = 3 ; :: thesis: ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x
A67: M * (<*rf*> @) is Matrix of 3,1,F_Real by A16, EUCLID_8:50, Th74;
then A68: Indices (M * (<*rf*> @)) = [:(Seg 3),(Seg 1):] by MATRIX_0:23;
A69: now :: thesis: ( len rt = 3 & <*((Line ((M * PQR),1)) . 3)*> = rt . 1 & <*((Line ((M * PQR),2)) . 3)*> = rt . 2 & <*((Line ((M * PQR),3)) . 3)*> = rt . 3 )
thus len rt = 3 by A19; :: thesis: ( <*((Line ((M * PQR),1)) . 3)*> = rt . 1 & <*((Line ((M * PQR),2)) . 3)*> = rt . 2 & <*((Line ((M * PQR),3)) . 3)*> = rt . 3 )
<*((M * PQR) * (1,3))*> = rt . 1
proof
( 1 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then A70: ( width M = len PQR & [1,3] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A71: (M * (<*rf*> @)) . 1 = <*((Line (M,1)) "*" (Col (PQR,3)))*>
proof
A72: 1 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*rf*> @)),1) = <*((Line (M,1)) "*" (Col (PQR,3)))*>
proof
( 1 in Seg 3 & 1 in Seg 1 ) by FINSEQ_1:1;
then A73: [1,1] in Indices (M * (<*rf*> @)) by A68, ZFMISC_1:87;
len rf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*rf*> @)),1) = <*((M * (<*rf*> @)) * (1,1))*> by Th75
.= <*((Line (M,1)) "*" (Col ((<*rf*> @),1)))*> by A18, A73, MATRIX_3:def 4
.= <*((Line (M,1)) "*" rf)*> by Th76
.= <*((Line (M,1)) "*" (Col (PQR,3)))*> by A15, A9, A10, MATRIX_0:57, A4 ;
hence Line ((M * (<*rf*> @)),1) = <*((Line (M,1)) "*" (Col (PQR,3)))*> ; :: thesis: verum
end;
hence (M * (<*rf*> @)) . 1 = <*((Line (M,1)) "*" (Col (PQR,3)))*> by A72, A67, MATRIX_0:52; :: thesis: verum
end;
rt . 1 = (M * (<*rf*> @)) . 1 by A7, LAPLACE:def 9;
hence <*((M * PQR) * (1,3))*> = rt . 1 by A70, MATRIX_3:def 4, A71; :: thesis: verum
end;
hence <*((Line ((M * PQR),1)) . 3)*> = rt . 1 by A24, MATRIX_0:def 7; :: thesis: ( <*((Line ((M * PQR),2)) . 3)*> = rt . 2 & <*((Line ((M * PQR),3)) . 3)*> = rt . 3 )
<*((M * PQR) * (2,3))*> = rt . 2
proof
( 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then A74: ( width M = len PQR & [2,3] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A75: (M * (<*rf*> @)) . 2 = <*((Line (M,2)) "*" (Col (PQR,3)))*>
proof
A76: 2 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*rf*> @)),2) = <*((Line (M,2)) "*" (Col (PQR,3)))*>
proof
( 1 in Seg 1 & 2 in Seg 3 ) by FINSEQ_1:1;
then A77: [2,1] in Indices (M * (<*rf*> @)) by A68, ZFMISC_1:87;
len rf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*rf*> @)),2) = <*((M * (<*rf*> @)) * (2,1))*> by Th75
.= <*((Line (M,2)) "*" (Col ((<*rf*> @),1)))*> by A18, A77, MATRIX_3:def 4
.= <*((Line (M,2)) "*" rf)*> by Th76
.= <*((Line (M,2)) "*" (Col (PQR,3)))*> by A15, A9, A10, MATRIX_0:57, A4 ;
hence Line ((M * (<*rf*> @)),2) = <*((Line (M,2)) "*" (Col (PQR,3)))*> ; :: thesis: verum
end;
hence (M * (<*rf*> @)) . 2 = <*((Line (M,2)) "*" (Col (PQR,3)))*> by A76, A67, MATRIX_0:52; :: thesis: verum
end;
rt . 2 = (M * (<*rf*> @)) . 2 by A7, LAPLACE:def 9;
hence <*((M * PQR) * (2,3))*> = rt . 2 by A74, MATRIX_3:def 4, A75; :: thesis: verum
end;
hence <*((Line ((M * PQR),2)) . 3)*> = rt . 2 by A24, MATRIX_0:def 7; :: thesis: <*((Line ((M * PQR),3)) . 3)*> = rt . 3
<*((M * PQR) * (3,3))*> = rt . 3
proof
3 in Seg 3 by FINSEQ_1:1;
then A78: ( width M = len PQR & [3,3] in Indices (M * PQR) ) by A9, MATRIX_0:23, A11, ZFMISC_1:87;
A79: (M * (<*rf*> @)) . 3 = <*((Line (M,3)) "*" (Col (PQR,3)))*>
proof
A80: 3 in Seg 3 by FINSEQ_1:1;
Line ((M * (<*rf*> @)),3) = <*((Line (M,3)) "*" (Col (PQR,3)))*>
proof
( 1 in Seg 1 & 3 in Seg 3 ) by FINSEQ_1:1;
then A81: [3,1] in Indices (M * (<*rf*> @)) by A68, ZFMISC_1:87;
len rf = 3 by A16, EUCLID_8:50;
then Line ((M * (<*rf*> @)),3) = <*((M * (<*rf*> @)) * (3,1))*> by Th75
.= <*((Line (M,3)) "*" (Col ((<*rf*> @),1)))*> by A18, A81, MATRIX_3:def 4
.= <*((Line (M,3)) "*" rf)*> by Th76
.= <*((Line (M,3)) "*" (Col (PQR,3)))*> by A15, A9, A10, MATRIX_0:57, A4 ;
hence Line ((M * (<*rf*> @)),3) = <*((Line (M,3)) "*" (Col (PQR,3)))*> ; :: thesis: verum
end;
hence (M * (<*rf*> @)) . 3 = <*((Line (M,3)) "*" (Col (PQR,3)))*> by A80, A67, MATRIX_0:52; :: thesis: verum
end;
rt . 3 = (M * (<*rf*> @)) . 3 by A7, LAPLACE:def 9;
hence <*((M * PQR) * (3,3))*> = rt . 3 by A78, MATRIX_3:def 4, A79; :: thesis: verum
end;
hence <*((Line ((M * PQR),3)) . 3)*> = rt . 3 by A24, MATRIX_0:def 7; :: thesis: verum
end;
A82: ( (Line ((M * PQR),1)) . 3 = (M * PQR) * (1,3) & (Line ((M * PQR),2)) . 3 = (M * PQR) * (2,3) & (Line ((M * PQR),3)) . 3 = (M * PQR) * (3,3) ) by A24, MATRIX_0:def 7;
( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then ( [1,3] in Indices (M * PQR) & [2,3] in Indices (M * PQR) & [3,3] in Indices (M * PQR) ) by A11, ZFMISC_1:87;
then A83: ( ((M * PQR) @) * (3,1) = (M * PQR) * (1,3) & ((M * PQR) @) * (3,2) = (M * PQR) * (2,3) & ((M * PQR) @) * (3,3) = (M * PQR) * (3,3) ) by MATRIX_0:def 6;
width ((M * PQR) @) = len (M * PQR) by A21, MATRIX_0:29;
then Seg (width ((M * PQR) @)) = dom (M * PQR) by FINSEQ_1:def 3;
then A84: ( (Line (((M * PQR) @),3)) . 1 = ((M * PQR) @) * (3,1) & (Line (((M * PQR) @),3)) . 2 = ((M * PQR) @) * (3,2) & (Line (((M * PQR) @),3)) . 3 = ((M * PQR) @) * (3,3) ) by A20, FINSEQ_1:1, MATRIX_0:def 7;
3 in Seg 3 by FINSEQ_1:1;
then A85: ((M * PQR) @) . 3 = Line (((M * PQR) @),3) by MATRIX_0:52;
reconsider FMPQR = Line (((M * PQR) @),3) as FinSequence of REAL ;
width ((M * PQR) @) = 3 by MATRIX_0:23;
then A86: len FMPQR = 3 by MATRIX_0:def 7;
then A87: <*<*((Line (((M * PQR) @),3)) . 1)*>,<*((Line (((M * PQR) @),3)) . 2)*>,<*((Line (((M * PQR) @),3)) . 3)*>*> = F2M FMPQR by DEF1;
FMPQR = M2F (F2M FMPQR) by A86, Th70
.= M2F rt by A87, A84, A83, A69, FINSEQ_1:45, A82 ;
hence ((M * PQR) @) . x = <*(M2F pt),(M2F qt),(M2F rt)*> . x by A85, A66, FINSEQ_1:45; :: thesis: verum
end;
end;
end;
end;
hence (M * PQR) @ = <*(M2F pt),(M2F qt),(M2F rt)*> by FUNCT_1:def 11; :: thesis: verum