let i be Nat; :: thesis: for v being Element of (TOP-REAL 3)
for pf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds
(Line (N,i)) "*" pf = ((N * pf) . i) . 1
let v be Element of (TOP-REAL 3); :: thesis: for pf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds
(Line (N,i)) "*" pf = ((N * pf) . i) . 1
let pf be FinSequence of F_Real; :: thesis: for N being Matrix of 3,F_Real st i in Seg 3 & pf = v holds
(Line (N,i)) "*" pf = ((N * pf) . i) . 1
let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & pf = v implies (Line (N,i)) "*" pf = ((N * pf) . i) . 1 )
assume that
A1: i in Seg 3 and
A2: pf = v ; :: thesis: (Line (N,i)) "*" pf = ((N * pf) . i) . 1
A3: N * (<*pf*> @) is Matrix of 3,1,F_Real by A2, FINSEQ_3:153, ANPROJ_8:91;
v in TOP-REAL 3 ;
then v in REAL 3 by EUCLID:22;
then A4: 3 = len pf by A2, EUCLID_8:50;
v in TOP-REAL 3 ;
then A5: v in REAL 3 by EUCLID:22;
A6: width <*pf*> = len pf by ANPROJ_8:75
.= 3 by A2, A5, EUCLID_8:50 ;
A7: width N = 3 by MATRIX_0:24
.= len (<*pf*> @) by MATRIX_0:def 6, A6 ;
N * (<*pf*> @) is Matrix of 3,1,F_Real by A2, FINSEQ_3:153, ANPROJ_8:91;
then A8: ( [1,1] in Indices (N * (<*pf*> @)) & [2,1] in Indices (N * (<*pf*> @)) & [3,1] in Indices (N * (<*pf*> @)) ) by MATRIX_0:23, ANPROJ_8:2;
A9: not not i = 1 & ... & not i = 3 by A1, FINSEQ_1:91;
(N * pf) . i = (N * (<*pf*> @)) . i by LAPLACE:def 9
.= Line ((N * (<*pf*> @)),i) by A1, A3, MATRIX_0:52
.= <*((N * (<*pf*> @)) * (i,1))*> by A9, A4, ANPROJ_8:92 ;
then ((N * pf) . i) . 1 = (N * (<*pf*> @)) * (i,1)
.= (Line (N,i)) "*" (Col ((<*pf*> @),1)) by A9, A7, A8, MATRIX_3:def 4 ;
hence (Line (N,i)) "*" pf = ((N * pf) . i) . 1 by ANPROJ_8:93; :: thesis: verum