let i be Nat; :: thesis: for r being Real
for u, v being Element of (TOP-REAL 3)
for p1 being FinSequence of 1 -tuples_on REAL
for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds
(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)
let r be Real; :: thesis: for u, v being Element of (TOP-REAL 3)
for p1 being FinSequence of 1 -tuples_on REAL
for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds
(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)
let u, v be Element of (TOP-REAL 3); :: thesis: for p1 being FinSequence of 1 -tuples_on REAL
for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds
(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)
let p1 be FinSequence of 1 -tuples_on REAL; :: thesis: for pf, uf being FinSequence of F_Real
for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds
(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)
let pf, uf be FinSequence of F_Real; :: thesis: for N being Matrix of 3,F_Real st i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u holds
(p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)
let N be Matrix of 3,F_Real; :: thesis: ( i in Seg 3 & u = uf & pf = v & p1 = N * uf & r <> 0 & v = r * u implies (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf) )
assume that
A1: i in Seg 3 and
A2: u = uf and
A3: pf = v and
A4: p1 = N * uf and
A5: r <> 0 and
A6: v = r * u ; :: thesis: (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf)
set b = 1 / r;
A7: ( p1 . 1 = <*((N * (<*uf*> @)) * (1,1))*> & p1 . 2 = <*((N * (<*uf*> @)) * (2,1))*> & p1 . 3 = <*((N * (<*uf*> @)) * (3,1))*> ) by A2, A4, FINSEQ_1:1, Lem02;
not not i = 1 & ... & not i = 3 by A1, FINSEQ_1:91;
then (p1 . i) . 1 = (N * (<*uf*> @)) * (i,1) by A7
.= (1 / r) * ((Line (N,i)) "*" pf) by A1, A2, A3, A5, A6, Lem03 ;
hence (p1 . i) . 1 = (1 / r) * ((Line (N,i)) "*" pf) ; :: thesis: verum