let s be Element of (ProjectiveSpace (TOP-REAL 3)); for p, q, r being Element of absolute st p,q,r are_mutually_distinct & s in (tangent p) /\ (tangent q) holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )
let p, q, r be Element of absolute ; ( p,q,r are_mutually_distinct & s in (tangent p) /\ (tangent q) implies ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s ) )
assume that
A1:
p,q,r are_mutually_distinct
and
A2:
s in (tangent p) /\ (tangent q)
; ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )
reconsider P1 = p, P2 = q, P3 = r, P4 = s as Point of real_projective_plane ;
( P4 in tangent p & P4 in tangent q )
by A2, XBOOLE_0:def 4;
then
( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear )
by A1, Th27;
then consider N being invertible Matrix of 3,F_Real such that
A3:
(homography N) . Dir101 = P1
and
A4:
(homography N) . Dirm101 = P2
and
A5:
(homography N) . Dir011 = P3
and
A6:
(homography N) . Dir010 = P4
by BKMODEL1:44, ANPROJ_9:31;
consider na, nb, nc, nd, ne, nf, ng, nh, ni being Element of F_Real such that
A7:
N = <*<*na,nb,nc*>,<*nd,ne,nf*>,<*ng,nh,ni*>*>
by PASCAL:3;
reconsider b = - 1 as Element of F_Real by XREAL_0:def 1;
A8:
not b is zero
;
reconsider a = 1 as Element of F_Real ;
not a is zero
;
then reconsider a = 1, b = - 1 as non zero Element of F_Real by A8;
reconsider N1 = <*<*a,0,0*>,<*0,a,0*>,<*0,0,b*>*> as invertible Matrix of 3,F_Real by ANPROJ_9:9;
reconsider M = ((N @) * N1) * N as invertible Matrix of 3,F_Real ;
A9:
N1 = symmetric_3 (a,a,b,0,0,0)
by PASCAL:def 3;
then A10:
M is symmetric
by PASCAL:7, PASCAL:12;
consider va, vb, vc, vd, ve, vf, vg, vh, vi being Element of F_Real such that
A11:
M = <*<*va,vb,vc*>,<*vd,ve,vf*>,<*vg,vh,vi*>*>
by PASCAL:3;
A12:
( vb = vd & vc = vg & vh = vf )
by A10, A11, PASCAL:6;
reconsider ra = va, rb = vb, rc = vc, re = ve, rf = vf, ri = vi as Real ;
A13:
M = symmetric_3 (ra,re,ri,rb,rc,rf)
by A12, A11, PASCAL:def 3;
A14:
( p in conic (1,1,(- 1),0,0,0) & N ~ is invertible )
;
reconsider NR = MXF2MXR (N ~) as Matrix of 3,REAL by MATRIXR1:def 2;
A15:
N1 = symmetric_3 (1,1,(- 1),(0 / 2),(0 / 2),(0 / 2))
by PASCAL:def 3;
reconsider N2 = N1 as Matrix of 3,REAL ;
A16:
M = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * N2) * (MXF2MXR ((MXR2MXF NR) ~))
by A15, BKMODEL1:53;
A17:
(homography (N ~)) . p = Dir101
by A3, ANPROJ_9:15;
A18:
( ( not ra = 0 or not re = 0 or not ri = 0 or not rb = 0 or not rc = 0 or not rf = 0 ) & (homography (N ~)) . p in conic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf)) )
by A13, A14, A15, A16, PASCAL:16;
Dir101 in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 }
by A18, A17, PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A19:
Dir101 = Q
and
A20:
for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0
;
A21:
( |[1,0,1]| . 1 = 1 & |[1,0,1]| . 2 = 0 & |[1,0,1]| . 3 = 1 )
;
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),|[1,0,1]|) = 0
by A19, A20, BKMODEL1:41;
then A22: 0 =
((((((ra * 1) * 1) + ((re * 0) * 0)) + ((ri * 1) * 1)) + (((2 * rb) * 1) * 0)) + (((2 * rc) * 1) * 1)) + (((2 * rf) * 0) * 1)
by A21, PASCAL:def 1
.=
(ra + ri) + (2 * rc)
;
A23:
(homography (N ~)) . q = Dirm101
by A4, ANPROJ_9:15;
( q in conic (1,1,(- 1),0,0,0) & N ~ is invertible )
;
then A25:
( ( not ra = 0 or not re = 0 or not ri = 0 or not rb = 0 or not rc = 0 or not rf = 0 ) & (homography (N ~)) . q in conic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf)) )
by A13, PASCAL:16, A15, A16;
Dirm101 in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 }
by A23, A25, PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A26:
Dirm101 = Q
and
A27:
for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0
;
A28:
( |[(- 1),0,1]| . 1 = - 1 & |[(- 1),0,1]| . 2 = 0 & |[(- 1),0,1]| . 3 = 1 )
;
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),|[(- 1),0,1]|) = 0
by A26, A27, BKMODEL1:41;
then A29: 0 =
((((((ra * (- 1)) * (- 1)) + ((re * 0) * 0)) + ((ri * 1) * 1)) + (((2 * rb) * (- 1)) * 0)) + (((2 * rc) * (- 1)) * 1)) + (((2 * rf) * 0) * 1)
by A28, PASCAL:def 1
.=
(ra + ri) - (2 * rc)
;
A30:
(homography (N ~)) . r = Dir011
by A5, ANPROJ_9:15;
( r in conic (1,1,(- 1),0,0,0) & N ~ is invertible )
;
then A31:
for fa, fb, fc, fe, fi, ff being Real
for N1, M, NR being Matrix of 3,REAL st N1 = symmetric_3 (1,1,(- 1),(0 / 2),(0 / 2),(0 / 2)) & NR = MXF2MXR (N ~) & M = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * N1) * (MXF2MXR ((MXR2MXF NR) ~)) & M = symmetric_3 (fa,fe,fi,fb,fc,ff) holds
( ( not fa = 0 or not fe = 0 or not fi = 0 or not fb = 0 or not ff = 0 or not fc = 0 ) & (homography (N ~)) . r in conic (fa,fe,fi,(2 * fb),(2 * fc),(2 * ff)) )
by PASCAL:16;
( ( not ra = 0 or not re = 0 or not ri = 0 or not rb = 0 or not rc = 0 or not rf = 0 ) & (homography (N ~)) . r in conic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf)) )
by A9, A13, A31, A16;
then
Dir011 in { P where P is Point of (ProjectiveSpace (TOP-REAL 3)) : for u being Element of (TOP-REAL 3) st not u is zero & P = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0 }
by A30, PASCAL:def 2;
then consider Q being Point of (ProjectiveSpace (TOP-REAL 3)) such that
A32:
Dir011 = Q
and
A33:
for u being Element of (TOP-REAL 3) st not u is zero & Q = Dir u holds
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),u) = 0
;
A34:
( |[0,1,1]| . 1 = 0 & |[0,1,1]| . 2 = 1 & |[0,1,1]| . 3 = 1 )
;
qfconic (ra,re,ri,(2 * rb),(2 * rc),(2 * rf),|[0,1,1]|) = 0
by A32, A33, BKMODEL1:41;
then A35: 0 =
((((((ra * 0) * 0) + ((re * 1) * 1)) + ((ri * 1) * 1)) + (((2 * rb) * 0) * 1)) + (((2 * rc) * 0) * 1)) + (((2 * rf) * 1) * 1)
by A34, PASCAL:def 1
.=
(re + ri) + (2 * rf)
;
( rc = 0 & ra = - ri & rb = 0 & rf = 0 & ra = re )
proof
thus
rc = 0
by A22, A29;
( ra = - ri & rb = 0 & rf = 0 & ra = re )
thus
ra = - ri
by A22, A29;
( rb = 0 & rf = 0 & ra = re )
consider k1 being
Element of
(TOP-REAL 3) such that A36:
not
k1 is
zero
and A37:
P1 = Dir k1
by ANPROJ_1:26;
consider k1b being
Element of
(TOP-REAL 3) such that A38:
not
k1b is
zero
and A39:
P2 = Dir k1b
by ANPROJ_1:26;
consider k2 being
Element of
(TOP-REAL 3) such that A40:
not
k2 is
zero
and A41:
P4 = Dir k2
by ANPROJ_1:26;
reconsider kf1 =
k1,
kf1b =
k1b,
kf2 =
k2 as
FinSequence of
REAL by EUCLID:24;
A42:
(
P4 in tangent p &
N2 is
Matrix of 3,
REAL &
p is
Element of
absolute &
Q is
Element of
real_projective_plane &
k1 is non
zero Element of
(TOP-REAL 3) &
k2 is non
zero Element of
(TOP-REAL 3) &
kf1 is
FinSequence of
REAL &
kf2 is
FinSequence of
REAL &
N2 = symmetric_3 (1,1,
(- 1),
0,
0,
0) &
p = Dir k1 &
P4 = Dir k2 &
k1 = kf1 &
k2 = kf2 )
by A2, XBOOLE_0:def 4, PASCAL:def 3, A36, A37, A40, A41;
A43:
(
P4 in tangent q &
N2 is
Matrix of 3,
REAL &
p is
Element of
absolute &
k1b is non
zero Element of
(TOP-REAL 3) &
k2 is non
zero Element of
(TOP-REAL 3) &
kf1b is
FinSequence of
REAL &
kf2 is
FinSequence of
REAL &
N2 = symmetric_3 (1,1,
(- 1),
0,
0,
0) &
q = Dir k1b &
P4 = Dir k2 &
k1b = kf1b &
k2 = kf2 )
by A2, A38, A40, PASCAL:def 3, A39, A41, XBOOLE_0:def 4;
consider ua,
va being
Element of
(TOP-REAL 3),
ufa being
FinSequence of
F_Real,
pa being
FinSequence of 1
-tuples_on REAL such that A44:
(
Dir101 = Dir ua & not
ua is
zero &
ua = ufa &
pa = N * ufa &
va = M2F pa & not
va is
zero &
(homography N) . Dir101 = Dir va )
by ANPROJ_8:def 4;
are_Prop k1,
va
by A3, A37, A44, ANPROJ_1:22, A36;
then consider li being
Real such that A45:
li <> 0
and A46:
k1 = li * va
by ANPROJ_1:1;
A47:
len (N * (<*ufa*> @)) = len N
A51:
len pa =
len N
by A47, A44, LAPLACE:def 9
.=
3
by MATRIX_0:23
;
then A52:
kf1 = M2F (li * pa)
by A44, A46, ANPROJ_8:83;
consider ub,
vb being
Element of
(TOP-REAL 3),
ufb being
FinSequence of
F_Real,
pb being
FinSequence of 1
-tuples_on REAL such that A53:
(
Dir010 = Dir ub & not
ub is
zero &
ub = ufb &
pb = N * ufb &
vb = M2F pb & not
vb is
zero &
(homography N) . Dir010 = Dir vb )
by ANPROJ_8:def 4;
are_Prop ub,
|[0,1,0]|
by A53, ANPROJ_1:22, ANPROJ_9:def 6, ANPROJ_9:10;
then consider lub being
Real such that A54:
lub <> 0
and A55:
ub = lub * |[0,1,0]|
by ANPROJ_1:1;
A56:
ufb =
|[(lub * 0),(lub * 1),(lub * 0)]|
by A53, A55, EUCLID_5:8
.=
|[0,lub,0]|
;
lub in REAL
by XREAL_0:def 1;
then reconsider MUFB =
<*ufb*> as
Matrix of 1,3,
F_Real by A56, BKMODEL1:27;
A57:
now ( MUFB * (1,1) = 0 & MUFB * (1,2) = lub & MUFB * (1,3) = 0 )
len ufb = 3
by A56, FINSEQ_1:45;
then
dom ufb = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
then
( 1
in dom ufb & 2
in dom ufb & 3
in dom ufb )
by ENUMSET1:def 1;
then
(
MUFB * (1,1)
= |[0,lub,0]| . 1 &
MUFB * (1,2)
= |[0,lub,0]| . 2 &
MUFB * (1,3)
= |[0,lub,0]| . 3 )
by A56, ANPROJ_8:70;
hence
(
MUFB * (1,1)
= 0 &
MUFB * (1,2)
= lub &
MUFB * (1,3)
= 0 )
;
verum end;
are_Prop k2,
vb
by A41, A6, A53, ANPROJ_1:22, A40;
then consider lj being
Real such that A58:
lj <> 0
and A59:
k2 = lj * vb
by ANPROJ_1:1;
A60:
len (N * (<*ufb*> @)) = len N
A62:
len pb =
len N
by A60, A53, LAPLACE:def 9
.=
3
by MATRIX_0:23
;
then A63:
M2F pb is
Element of
(TOP-REAL 3)
by ANPROJ_8:82;
then A64:
M2F pb is
Element of
REAL 3
by EUCLID:22;
then A65:
len (M2F pb) = 3
by EUCLID_8:50;
M2F pa is
Element of
(TOP-REAL 3)
by A51, ANPROJ_8:82;
then A66:
M2F pa is
Element of
REAL 3
by EUCLID:22;
then A67:
len (M2F pa) = 3
by EUCLID_8:50;
A68:
li * (N2 * (M2F pa)) = N2 * (li * (M2F pa))
A69:
(
len (li * (N2 * (M2F pa))) = 3 &
len (N2 * (M2F pa)) = 3 )
then A72:
len (M2F pb) = len (N2 * (M2F (li * pa)))
by A51, ANPROJ_8:83, A68, A65;
A73:
len (M2F pb) = len (N2 * (M2F pa))
by A69, A64, EUCLID_8:50;
A74:
kf2 = M2F (lj * pb)
by A59, A53, A62, ANPROJ_8:83;
A75:
(
len (M2F (lj * pb)) = len N2 &
len (M2F (li * pa)) = width N2 &
len (M2F (li * pa)) > 0 )
proof
A76:
(
len N2 = 3 &
width N2 = 3 )
by MATRIX_0:23;
consider p1,
p2,
p3 being
Real such that A77:
(
p1 = (pb . 1) . 1 &
p2 = (pb . 2) . 1 &
p3 = (pb . 3) . 1 &
lj * pb = <*<*(lj * p1)*>,<*(lj * p2)*>,<*(lj * p3)*>*> )
by A62, ANPROJ_8:def 3;
len (lj * pb) = 3
by A77, FINSEQ_1:45;
then A78:
M2F (lj * pb) = <*(((lj * pb) . 1) . 1),(((lj * pb) . 2) . 1),(((lj * pb) . 3) . 1)*>
by ANPROJ_8:def 2;
consider p1,
p2,
p3 being
Real such that A79:
(
p1 = (pa . 1) . 1 &
p2 = (pa . 2) . 1 &
p3 = (pa . 3) . 1 &
li * pa = <*<*(li * p1)*>,<*(li * p2)*>,<*(li * p3)*>*> )
by A51, ANPROJ_8:def 3;
len (li * pa) = 3
by A79, FINSEQ_1:45;
then
M2F (li * pa) = <*(((li * pa) . 1) . 1),(((li * pa) . 2) . 1),(((li * pa) . 3) . 1)*>
by ANPROJ_8:def 2;
hence
(
len (M2F (lj * pb)) = len N2 &
len (M2F (li * pa)) = width N2 &
len (M2F (li * pa)) > 0 )
by A76, A78, FINSEQ_1:45;
verum
end;
A80:
0 =
SumAll (QuadraticForm ((M2F (lj * pb)),N2,(M2F (li * pa))))
by A42, Th26, A52, A74
.=
|((M2F (lj * pb)),(N2 * (M2F (li * pa))))|
by A75, MATRPROB:44
.=
|((lj * (M2F pb)),(N2 * (M2F (li * pa))))|
by A62, ANPROJ_8:83
.=
lj * |((M2F pb),(N2 * (M2F (li * pa))))|
by A72, RVSUM_1:121
.=
lj * |((M2F pb),(li * (N2 * (M2F pa))))|
by A68, A51, ANPROJ_8:83
.=
lj * (li * |((M2F pb),(N2 * (M2F pa)))|)
by A73, RVSUM_1:121
.=
(lj * li) * |((M2F pb),(N2 * (M2F pa)))|
;
A81:
(nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni)
proof
consider ua2,
va2 being
Element of
(TOP-REAL 3),
ufa2 being
FinSequence of
F_Real,
pa2 being
FinSequence of 1
-tuples_on REAL such that A82:
(
Dirm101 = Dir ua2 & not
ua2 is
zero &
ua2 = ufa2 &
pa2 = N * ufa2 &
va2 = M2F pa2 & not
va2 is
zero &
(homography N) . Dirm101 = Dir va2 )
by ANPROJ_8:def 4;
are_Prop k1b,
va2
by A39, A4, A82, ANPROJ_1:22, A38;
then consider li2 being
Real such that A83:
li2 <> 0
and A84:
k1b = li2 * va2
by ANPROJ_1:1;
A85:
len (N * (<*ufa2*> @)) = len N
A89:
len pa2 =
len N
by A85, A82, LAPLACE:def 9
.=
3
by MATRIX_0:23
;
A90:
kf1b = M2F (li2 * pa2)
by A82, A84, A89, ANPROJ_8:83;
M2F pa2 is
Element of
(TOP-REAL 3)
by A89, ANPROJ_8:82;
then A91:
M2F pa2 is
Element of
REAL 3
by EUCLID:22;
then A92:
len (M2F pa2) = 3
by EUCLID_8:50;
A93:
li2 * (N2 * (M2F pa2)) = N2 * (li2 * (M2F pa2))
A94:
(
len (li2 * (N2 * (M2F pa2))) = 3 &
len (N2 * (M2F pa2)) = 3 )
then A97:
len (M2F pb) = len (N2 * (M2F (li2 * pa2)))
by A89, ANPROJ_8:83, A93, A65;
A98:
len (M2F pb) = len (N2 * (M2F pa2))
by A94, A64, EUCLID_8:50;
A99:
kf2 = M2F (lj * pb)
by A59, A53, A62, ANPROJ_8:83;
A100:
(
len (M2F (lj * pb)) = len N2 &
len (M2F (li2 * pa2)) = width N2 &
len (M2F (li2 * pa2)) > 0 )
proof
A101:
(
len N2 = 3 &
width N2 = 3 )
by MATRIX_0:23;
consider p1,
p2,
p3 being
Real such that A102:
(
p1 = (pb . 1) . 1 &
p2 = (pb . 2) . 1 &
p3 = (pb . 3) . 1 &
lj * pb = <*<*(lj * p1)*>,<*(lj * p2)*>,<*(lj * p3)*>*> )
by A62, ANPROJ_8:def 3;
len (lj * pb) = 3
by A102, FINSEQ_1:45;
then A103:
M2F (lj * pb) = <*(((lj * pb) . 1) . 1),(((lj * pb) . 2) . 1),(((lj * pb) . 3) . 1)*>
by ANPROJ_8:def 2;
consider p1b,
p2b,
p3b being
Real such that A104:
(
p1b = (pa2 . 1) . 1 &
p2b = (pa2 . 2) . 1 &
p3b = (pa2 . 3) . 1 &
li2 * pa2 = <*<*(li2 * p1b)*>,<*(li2 * p2b)*>,<*(li2 * p3b)*>*> )
by A89, ANPROJ_8:def 3;
len (li2 * pa2) = 3
by A104, FINSEQ_1:45;
then
M2F (li2 * pa2) = <*(((li2 * pa2) . 1) . 1),(((li2 * pa2) . 2) . 1),(((li2 * pa2) . 3) . 1)*>
by ANPROJ_8:def 2;
hence
(
len (M2F (lj * pb)) = len N2 &
len (M2F (li2 * pa2)) = width N2 &
len (M2F (li2 * pa2)) > 0 )
by A101, A103, FINSEQ_1:45;
verum
end;
A105:
0 =
SumAll (QuadraticForm ((M2F (lj * pb)),N2,(M2F (li2 * pa2))))
by A43, Th26, A90, A99
.=
|((M2F (lj * pb)),(N2 * (M2F (li2 * pa2))))|
by A100, MATRPROB:44
.=
|((lj * (M2F pb)),(N2 * (M2F (li2 * pa2))))|
by A62, ANPROJ_8:83
.=
lj * |((M2F pb),(N2 * (M2F (li2 * pa2))))|
by A97, RVSUM_1:121
.=
lj * |((M2F pb),(li2 * (N2 * (M2F pa2))))|
by A93, A89, ANPROJ_8:83
.=
lj * (li2 * |((M2F pb),(N2 * (M2F pa2)))|)
by A98, RVSUM_1:121
.=
(lj * li2) * |((M2F pb),(N2 * (M2F pa2)))|
;
A106:
M2F pa2 = <*((pa2 . 1) . 1),((pa2 . 2) . 1),((pa2 . 3) . 1)*>
by A89, ANPROJ_8:def 2;
dom (M2F pa2) = Seg 3
by A91, EUCLID_8:50;
then
(
(M2F pa2) . 1
in REAL &
(M2F pa2) . 2
in REAL &
(M2F pa2) . 3
in REAL )
by FINSEQ_1:1, FINSEQ_2:11;
then reconsider s1 =
(pa2 . 1) . 1,
s2 =
(pa2 . 2) . 1,
s3 =
(pa2 . 3) . 1 as
Element of
REAL by A106;
A107:
M2F pb = <*((pb . 1) . 1),((pb . 2) . 1),((pb . 3) . 1)*>
by A62, ANPROJ_8:def 2;
dom (M2F pb) = Seg 3
by A64, EUCLID_8:50;
then
(
(M2F pb) . 1
in REAL &
(M2F pb) . 2
in REAL &
(M2F pb) . 3
in REAL )
by FINSEQ_1:1, FINSEQ_2:11;
then reconsider t1 =
(pb . 1) . 1,
t2 =
(pb . 2) . 1,
t3 =
(pb . 3) . 1 as
Element of
F_Real by A107;
reconsider r1 = 1,
r2 =
0 ,
r3 =
- 1 as
Element of
F_Real by XREAL_0:def 1;
(nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni)
proof
reconsider r1 = 1,
r2 =
0 ,
r3 =
- 1 as
Element of
F_Real by XREAL_0:def 1;
A108:
M2F pa2 = <*((pa2 . 1) . 1),((pa2 . 2) . 1),((pa2 . 3) . 1)*>
by A89, ANPROJ_8:def 2;
dom (M2F pa2) = Seg 3
by A91, EUCLID_8:50;
then
(
(M2F pa2) . 1
in REAL &
(M2F pa2) . 2
in REAL &
(M2F pa2) . 3
in REAL )
by FINSEQ_1:1, FINSEQ_2:11;
then reconsider s1 =
(pa2 . 1) . 1,
s2 =
(pa2 . 2) . 1,
s3 =
(pa2 . 3) . 1 as
Element of
REAL by A108;
A109:
M2F pb = <*((pb . 1) . 1),((pb . 2) . 1),((pb . 3) . 1)*>
by A62, ANPROJ_8:def 2;
dom (M2F pb) = Seg 3
by A64, EUCLID_8:50;
then
(
(M2F pb) . 1
in REAL &
(M2F pb) . 2
in REAL &
(M2F pb) . 3
in REAL )
by FINSEQ_1:1, FINSEQ_2:11;
then reconsider t1 =
(pb . 1) . 1,
t2 =
(pb . 2) . 1,
t3 =
(pb . 3) . 1 as
Element of
F_Real by A109;
M2F pa2 = <*s1,s2,s3*>
by A89, ANPROJ_8:def 2;
then A110:
N2 * (M2F pa2) =
<*(((1 * s1) + (0 * s2)) + (0 * s3)),(((0 * s1) + (1 * s2)) + (0 * s3)),(((0 * s1) + (0 * s2)) + ((- 1) * s3))*>
by PASCAL:9
.=
<*s1,s2,(- s3)*>
;
M2F pb = <*t1,t2,t3*>
by A62, ANPROJ_8:def 2;
then A111:
(
(M2F pb) . 1
= t1 &
(M2F pb) . 2
= t2 &
(M2F pb) . 3
= t3 &
<*s1,s2,(- s3)*> . 1
= s1 &
<*s1,s2,(- s3)*> . 2
= s2 &
<*s1,s2,(- s3)*> . 3
= - s3 )
;
A112:
M2F pb is
Element of
REAL 3
by A63, EUCLID:22;
A113:
|[s1,s2,(- s3)]| is
Element of
REAL 3
by EUCLID:22;
0 =
|((M2F pb),<*s1,s2,(- s3)*>)|
by A110, A105, A83, A58
.=
((t1 * s1) + (t2 * s2)) + (t3 * (- s3))
by A112, A113, EUCLID_8:63, A111
;
then A114:
(t1 * s1) + (t2 * s2) = t3 * s3
;
not
|[(- 1),0,1]| is
zero
by EUCLID_5:4, FINSEQ_1:78;
then
are_Prop ua2,
|[(- 1),0,1]|
by A82, ANPROJ_1:22;
then consider lua2 being
Real such that A115:
lua2 <> 0
and A116:
ua2 = lua2 * |[(- 1),0,1]|
by ANPROJ_1:1;
A117:
ua2 =
|[(lua2 * (- 1)),(lua2 * 0),(lua2 * 1)]|
by A116, EUCLID_5:8
.=
|[(- lua2),0,lua2]|
;
reconsider za1 =
- lua2,
za2 =
0 ,
za3 =
lua2 as
Element of
F_Real by XREAL_0:def 1;
(
lua2 in REAL &
- lua2 in REAL )
by XREAL_0:def 1;
then reconsider MUFA =
<*ufa2*> as
Matrix of 1,3,
F_Real by A117, A82, BKMODEL1:27;
now ( MUFA * (1,1) = - lua2 & MUFA * (1,2) = 0 & MUFA * (1,3) = lua2 )
len ufa2 = 3
by A117, A82, FINSEQ_1:45;
then
dom ufa2 = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
then
( 1
in dom ufa2 & 2
in dom ufa2 & 3
in dom ufa2 )
by ENUMSET1:def 1;
then
(
MUFA * (1,1)
= |[(- lua2),0,lua2]| . 1 &
MUFA * (1,2)
= |[(- lua2),0,lua2]| . 2 &
MUFA * (1,3)
= |[(- lua2),0,lua2]| . 3 )
by A117, A82, ANPROJ_8:70;
hence
(
MUFA * (1,1)
= - lua2 &
MUFA * (1,2)
= 0 &
MUFA * (1,3)
= lua2 )
;
verum end;
then A119:
<*ufa2*> @ = <*<*(- lua2)*>,<*0*>,<*lua2*>*>
by BKMODEL1:31;
reconsider nlua2 =
- lua2 as
Element of
F_Real by XREAL_0:def 1;
(
0 is
Element of
F_Real &
lua2 is
Element of
F_Real )
by XREAL_0:def 1;
then reconsider MUFAT =
<*<*nlua2*>,<*0*>,<*lua2*>*> as
Matrix of 3,1,
F_Real by BKMODEL1:28;
A120:
N * MUFAT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
A121:
N * ufa2 = N * MUFAT
by A119, LAPLACE:def 9;
then
N * ufa2 = <*<*((N * ufa2) * (1,1))*>,<*((N * ufa2) * (2,1))*>,<*((N * ufa2) * (3,1))*>*>
by A120, BKMODEL1:30;
then A122:
(
pa2 . 1
= <*((N * ufa2) * (1,1))*> &
pa2 . 2
= <*((N * ufa2) * (2,1))*> &
pa2 . 3
= <*((N * ufa2) * (3,1))*> )
by A82;
N * MUFAT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
then A123:
Indices (N * MUFAT) = [:(Seg 3),(Seg 1):]
by MATRIX_0:23;
width N = 3
by MATRIX_0:24;
then A124:
width N = len MUFAT
by MATRIX_0:23;
A125:
Col (
MUFAT,1)
= <*za1,za2,za3*>
by ANPROJ_8:5;
A126:
(
Line (
N,1)
= <*na,nb,nc*> &
Line (
N,2)
= <*nd,ne,nf*> &
Line (
N,3)
= <*ng,nh,ni*> )
by A7, ANPROJ_9:4;
(
(N * MUFAT) * (1,1)
= (Line (N,1)) "*" (Col (MUFAT,1)) &
(N * MUFAT) * (2,1)
= (Line (N,2)) "*" (Col (MUFAT,1)) &
(N * MUFAT) * (3,1)
= (Line (N,3)) "*" (Col (MUFAT,1)) )
by A123, A124, MATRIX_3:def 4, ANPROJ_8:2;
then
(
(N * MUFAT) * (1,1)
= ((na * za1) + (nb * za2)) + (nc * za3) &
(N * MUFAT) * (2,1)
= ((nd * za1) + (ne * za2)) + (nf * za3) &
(N * MUFAT) * (3,1)
= ((ng * za1) + (nh * za2)) + (ni * za3) )
by A125, A126, ANPROJ_8:7;
then A127:
(
(pa2 . 1) . 1
= (na * nlua2) + (nc * lua2) &
(pa2 . 2) . 1
= (nd * nlua2) + (nf * lua2) &
(pa2 . 3) . 1
= (ng * nlua2) + (ni * lua2) )
by A121, A122;
reconsider z1 =
0 ,
z2 =
lub,
z3 =
0 as
Element of
F_Real by XREAL_0:def 1;
(
0 is
Element of
F_Real &
lub is
Element of
F_Real )
by XREAL_0:def 1;
then reconsider MUFBT =
<*<*0*>,<*lub*>,<*0*>*> as
Matrix of 3,1,
F_Real by BKMODEL1:28;
A128:
N * MUFBT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
A129:
N * ufb =
N * (<*ufb*> @)
by LAPLACE:def 9
.=
N * MUFBT
by A57, BKMODEL1:31
;
then
N * ufb = <*<*((N * ufb) * (1,1))*>,<*((N * ufb) * (2,1))*>,<*((N * ufb) * (3,1))*>*>
by A128, BKMODEL1:30;
then A130:
(
pb . 1
= <*((N * ufb) * (1,1))*> &
pb . 2
= <*((N * ufb) * (2,1))*> &
pb . 3
= <*((N * ufb) * (3,1))*> )
by A53;
N * MUFBT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
then A131:
Indices (N * MUFBT) = [:(Seg 3),(Seg 1):]
by MATRIX_0:23;
width N = 3
by MATRIX_0:24;
then A132:
width N = len MUFBT
by MATRIX_0:23;
reconsider z1 =
0 ,
z2 =
lub,
z3 =
0 as
Element of
F_Real by XREAL_0:def 1;
A133:
Col (
MUFBT,1)
= <*z1,z2,z3*>
by ANPROJ_8:5;
A134:
(
Line (
N,1)
= <*na,nb,nc*> &
Line (
N,2)
= <*nd,ne,nf*> &
Line (
N,3)
= <*ng,nh,ni*> )
by ANPROJ_9:4, A7;
(
(N * MUFBT) * (1,1)
= (Line (N,1)) "*" (Col (MUFBT,1)) &
(N * MUFBT) * (2,1)
= (Line (N,2)) "*" (Col (MUFBT,1)) &
(N * MUFBT) * (3,1)
= (Line (N,3)) "*" (Col (MUFBT,1)) )
by A132, MATRIX_3:def 4, A131, ANPROJ_8:2;
then
(
(N * MUFBT) * (1,1)
= ((na * z1) + (nb * z2)) + (nc * z3) &
(N * MUFBT) * (2,1)
= ((nd * z1) + (ne * z2)) + (nf * z3) &
(N * MUFBT) * (3,1)
= ((ng * z1) + (nh * z2)) + (ni * z3) )
by A133, A134, ANPROJ_8:7;
then
(
(pb . 1) . 1
= nb * lub &
(pb . 2) . 1
= ne * lub &
(pb . 3) . 1
= nh * lub )
by A129, A130;
then
((lua2 * lub) * (nb * ((- na) + nc))) + ((lua2 * lub) * (ne * ((- nd) + nf))) = (lua2 * lub) * (nh * ((- ng) + ni))
by A127, A114;
then
(((lua2 * lub) * (nb * ((- na) + nc))) + ((lua2 * lub) * (ne * ((- nd) + nf)))) - ((lua2 * lub) * (nh * ((- ng) + ni))) = 0
;
then
(lua2 * lub) * (((nb * ((- na) + nc)) + (ne * ((- nd) + nf))) - (nh * ((- ng) + ni))) = 0
;
then
((nb * ((- na) + nc)) + (ne * ((- nd) + nf))) - (nh * ((- ng) + ni)) = 0
by A54, A115;
hence
(nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni)
;
verum
end;
hence
(nb * ((- na) + nc)) + (ne * ((- nd) + nf)) = nh * ((- ng) + ni)
;
verum
end;
A136:
(nb * (na + nc)) + (ne * (nd + nf)) = nh * (ng + ni)
proof
reconsider r1 = 1,
r2 =
0 ,
r3 =
- 1 as
Element of
F_Real by XREAL_0:def 1;
A137:
M2F pa = <*((pa . 1) . 1),((pa . 2) . 1),((pa . 3) . 1)*>
by A51, ANPROJ_8:def 2;
dom (M2F pa) = Seg 3
by A66, EUCLID_8:50;
then
(
(M2F pa) . 1
in REAL &
(M2F pa) . 2
in REAL &
(M2F pa) . 3
in REAL )
by FINSEQ_1:1, FINSEQ_2:11;
then reconsider s1 =
(pa . 1) . 1,
s2 =
(pa . 2) . 1,
s3 =
(pa . 3) . 1 as
Element of
REAL by A137;
A138:
M2F pb = <*((pb . 1) . 1),((pb . 2) . 1),((pb . 3) . 1)*>
by A62, ANPROJ_8:def 2;
dom (M2F pb) = Seg 3
by A64, EUCLID_8:50;
then
(
(M2F pb) . 1
in REAL &
(M2F pb) . 2
in REAL &
(M2F pb) . 3
in REAL )
by FINSEQ_1:1, FINSEQ_2:11;
then reconsider t1 =
(pb . 1) . 1,
t2 =
(pb . 2) . 1,
t3 =
(pb . 3) . 1 as
Element of
F_Real by A138;
M2F pa = <*s1,s2,s3*>
by A51, ANPROJ_8:def 2;
then A139:
N2 * (M2F pa) =
<*(((1 * s1) + (0 * s2)) + (0 * s3)),(((0 * s1) + (1 * s2)) + (0 * s3)),(((0 * s1) + (0 * s2)) + ((- 1) * s3))*>
by PASCAL:9
.=
<*s1,s2,(- s3)*>
;
M2F pb = <*t1,t2,t3*>
by A62, ANPROJ_8:def 2;
then A140:
(
(M2F pb) . 1
= t1 &
(M2F pb) . 2
= t2 &
(M2F pb) . 3
= t3 &
<*s1,s2,(- s3)*> . 1
= s1 &
<*s1,s2,(- s3)*> . 2
= s2 &
<*s1,s2,(- s3)*> . 3
= - s3 )
;
A141:
M2F pb is
Element of
REAL 3
by A63, EUCLID:22;
A142:
|[s1,s2,(- s3)]| is
Element of
REAL 3
by EUCLID:22;
0 =
|((M2F pb),<*s1,s2,(- s3)*>)|
by A139, A80, A45, A58
.=
((t1 * s1) + (t2 * s2)) + (t3 * (- s3))
by A141, A142, EUCLID_8:63, A140
;
then A143:
(t1 * s1) + (t2 * s2) = t3 * s3
;
not
|[1,0,1]| is
zero
by EUCLID_5:4, FINSEQ_1:78;
then
are_Prop ua,
|[1,0,1]|
by A44, ANPROJ_1:22;
then consider lua being
Real such that A145:
lua <> 0
and A146:
ua = lua * |[1,0,1]|
by ANPROJ_1:1;
A147:
ua =
|[(lua * 1),(lua * 0),(lua * 1)]|
by A146, EUCLID_5:8
.=
|[lua,0,lua]|
;
reconsider za1 =
lua,
za2 =
0 ,
za3 =
lua as
Element of
F_Real by XREAL_0:def 1;
lua in REAL
by XREAL_0:def 1;
then reconsider MUFA =
<*ufa*> as
Matrix of 1,3,
F_Real by A147, A44, BKMODEL1:27;
now ( MUFA * (1,1) = lua & MUFA * (1,2) = 0 & MUFA * (1,3) = lua )
len ufa = 3
by A147, A44, FINSEQ_1:45;
then
dom ufa = {1,2,3}
by FINSEQ_1:def 3, FINSEQ_3:1;
then
( 1
in dom ufa & 2
in dom ufa & 3
in dom ufa )
by ENUMSET1:def 1;
then
(
MUFA * (1,1)
= |[lua,0,lua]| . 1 &
MUFA * (1,2)
= |[lua,0,lua]| . 2 &
MUFA * (1,3)
= |[lua,0,lua]| . 3 )
by A147, A44, ANPROJ_8:70;
hence
(
MUFA * (1,1)
= lua &
MUFA * (1,2)
= 0 &
MUFA * (1,3)
= lua )
;
verum end;
then A148:
<*ufa*> @ = <*<*lua*>,<*0*>,<*lua*>*>
by BKMODEL1:31;
(
0 is
Element of
F_Real &
lua is
Element of
F_Real )
by XREAL_0:def 1;
then reconsider MUFAT =
<*<*lua*>,<*0*>,<*lua*>*> as
Matrix of 3,1,
F_Real by BKMODEL1:28;
A149:
N * MUFAT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
A150:
N * ufa = N * MUFAT
by A148, LAPLACE:def 9;
N * ufa = <*<*((N * ufa) * (1,1))*>,<*((N * ufa) * (2,1))*>,<*((N * ufa) * (3,1))*>*>
by A149, A150, BKMODEL1:30;
then
(
pa . 1
= <*((N * ufa) * (1,1))*> &
pa . 2
= <*((N * ufa) * (2,1))*> &
pa . 3
= <*((N * ufa) * (3,1))*> )
by A44;
then A152:
(
(pa . 1) . 1
= (N * MUFAT) * (1,1) &
(pa . 2) . 1
= (N * MUFAT) * (2,1) &
(pa . 3) . 1
= (N * MUFAT) * (3,1) )
by A150;
N * MUFAT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
then A153:
Indices (N * MUFAT) = [:(Seg 3),(Seg 1):]
by MATRIX_0:23;
width N = 3
by MATRIX_0:24;
then A154:
width N = len MUFAT
by MATRIX_0:23;
A155:
Col (
MUFAT,1)
= <*za1,za2,za3*>
by ANPROJ_8:5;
A156:
(
Line (
N,1)
= <*na,nb,nc*> &
Line (
N,2)
= <*nd,ne,nf*> &
Line (
N,3)
= <*ng,nh,ni*> )
by ANPROJ_9:4, A7;
(
(N * MUFAT) * (1,1)
= (Line (N,1)) "*" (Col (MUFAT,1)) &
(N * MUFAT) * (2,1)
= (Line (N,2)) "*" (Col (MUFAT,1)) &
(N * MUFAT) * (3,1)
= (Line (N,3)) "*" (Col (MUFAT,1)) )
by A154, MATRIX_3:def 4, A153, ANPROJ_8:2;
then A157:
(
(pa . 1) . 1
= ((na * za1) + (nb * za2)) + (nc * za3) &
(pa . 2) . 1
= ((nd * za1) + (ne * za2)) + (nf * za3) &
(pa . 3) . 1
= ((ng * za1) + (nh * za2)) + (ni * za3) )
by A152, A155, A156, ANPROJ_8:7;
reconsider z1 =
0 ,
z2 =
lub,
z3 =
0 as
Element of
F_Real by XREAL_0:def 1;
(
0 is
Element of
F_Real &
lub is
Element of
F_Real )
by XREAL_0:def 1;
then reconsider MUFBT =
<*<*0*>,<*lub*>,<*0*>*> as
Matrix of 3,1,
F_Real by BKMODEL1:28;
A158:
N * MUFBT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
A159:
N * ufb =
N * (<*ufb*> @)
by LAPLACE:def 9
.=
N * MUFBT
by A57, BKMODEL1:31
;
N * ufb = <*<*((N * ufb) * (1,1))*>,<*((N * ufb) * (2,1))*>,<*((N * ufb) * (3,1))*>*>
by A158, A159, BKMODEL1:30;
then A160:
(
pb . 1
= <*((N * ufb) * (1,1))*> &
pb . 2
= <*((N * ufb) * (2,1))*> &
pb . 3
= <*((N * ufb) * (3,1))*> )
by A53;
N * MUFBT is
Matrix of 3,1,
F_Real
by BKMODEL1:24;
then A161:
Indices (N * MUFBT) = [:(Seg 3),(Seg 1):]
by MATRIX_0:23;
width N = 3
by MATRIX_0:24;
then A162:
width N = len MUFBT
by MATRIX_0:23;
reconsider z1 =
0 ,
z2 =
lub,
z3 =
0 as
Element of
F_Real by XREAL_0:def 1;
A163:
Col (
MUFBT,1)
= <*z1,z2,z3*>
by ANPROJ_8:5;
A164:
(
Line (
N,1)
= <*na,nb,nc*> &
Line (
N,2)
= <*nd,ne,nf*> &
Line (
N,3)
= <*ng,nh,ni*> )
by ANPROJ_9:4, A7;
(
(N * MUFBT) * (1,1)
= (Line (N,1)) "*" (Col (MUFBT,1)) &
(N * MUFBT) * (2,1)
= (Line (N,2)) "*" (Col (MUFBT,1)) &
(N * MUFBT) * (3,1)
= (Line (N,3)) "*" (Col (MUFBT,1)) )
by A162, MATRIX_3:def 4, A161, ANPROJ_8:2;
then
(
(N * MUFBT) * (1,1)
= ((na * z1) + (nb * z2)) + (nc * z3) &
(N * MUFBT) * (2,1)
= ((nd * z1) + (ne * z2)) + (nf * z3) &
(N * MUFBT) * (3,1)
= ((ng * z1) + (nh * z2)) + (ni * z3) )
by A163, A164, ANPROJ_8:7;
then
(
(pb . 1) . 1
= nb * lub &
(pb . 2) . 1
= ne * lub &
(pb . 3) . 1
= nh * lub )
by A160, A159;
then
((lua * lub) * (nb * (na + nc))) + ((lua * lub) * (ne * (nd + nf))) = (lua * lub) * (nh * (ng + ni))
by A157, A143;
then
(((lua * lub) * (nb * (na + nc))) + ((lua * lub) * (ne * (nd + nf)))) - ((lua * lub) * (nh * (ng + ni))) = 0
;
then
(lua * lub) * (((nb * (na + nc)) + (ne * (nd + nf))) - (nh * (ng + ni))) = 0
;
then
((nb * (na + nc)) + (ne * (nd + nf))) - (nh * (ng + ni)) = 0
by A54, A145;
hence
(nb * (na + nc)) + (ne * (nd + nf)) = nh * (ng + ni)
;
verum
end;
<*<*na,nb,nc*>,<*nd,ne,nf*>,<*ng,nh,ni*>*> = <*<*(N * (1,1)),(N * (1,2)),(N * (1,3))*>,<*(N * (2,1)),(N * (2,2)),(N * (2,3))*>,<*(N * (3,1)),(N * (3,2)),(N * (3,3))*>*>
by A7, MATRIXR2:37;
then A166:
(
na = N * (1,1) &
nb = N * (1,2) &
nc = N * (1,3) &
nd = N * (2,1) &
ne = N * (2,2) &
nf = N * (2,3) &
ng = N * (3,1) &
nh = N * (3,2) &
ni = N * (3,3) )
by PASCAL:2;
width N > 0
by MATRIX_0:23;
then
(
len N = 3 &
len N1 = 3 &
width N1 = 3 &
width (N @) = len N )
by MATRIX_0:29, MATRIX_0:23;
then A167:
<*<*ra,rb,rc*>,<*rb,re,rf*>,<*rc,rf,ri*>*> =
(N @) * (N1 * N)
by A12, A11, MATRIX_3:33
.=
<*<*(((N @) * (N1 * N)) * (1,1)),(((N @) * (N1 * N)) * (1,2)),(((N @) * (N1 * N)) * (1,3))*>,<*(((N @) * (N1 * N)) * (2,1)),(((N @) * (N1 * N)) * (2,2)),(((N @) * (N1 * N)) * (2,3))*>,<*(((N @) * (N1 * N)) * (3,1)),(((N @) * (N1 * N)) * (3,2)),(((N @) * (N1 * N)) * (3,3))*>*>
by MATRIXR2:37
;
A168:
(
((N @) * (N1 * N)) * (1,1)
= (((a * (N * (1,1))) * (N * (1,1))) + ((a * (N * (2,1))) * (N * (2,1)))) + ((b * (N * (3,1))) * (N * (3,1))) &
((N @) * (N1 * N)) * (1,2)
= (((a * (N * (1,1))) * (N * (1,2))) + ((a * (N * (2,1))) * (N * (2,2)))) + ((b * (N * (3,1))) * (N * (3,2))) &
((N @) * (N1 * N)) * (1,3)
= (((a * (N * (1,1))) * (N * (1,3))) + ((a * (N * (2,1))) * (N * (2,3)))) + ((b * (N * (3,1))) * (N * (3,3))) &
((N @) * (N1 * N)) * (2,1)
= (((a * (N * (1,2))) * (N * (1,1))) + ((a * (N * (2,2))) * (N * (2,1)))) + ((b * (N * (3,2))) * (N * (3,1))) &
((N @) * (N1 * N)) * (2,2)
= (((a * (N * (1,2))) * (N * (1,2))) + ((a * (N * (2,2))) * (N * (2,2)))) + ((b * (N * (3,2))) * (N * (3,2))) &
((N @) * (N1 * N)) * (2,3)
= (((a * (N * (1,2))) * (N * (1,3))) + ((a * (N * (2,2))) * (N * (2,3)))) + ((b * (N * (3,2))) * (N * (3,3))) &
((N @) * (N1 * N)) * (3,1)
= (((a * (N * (1,3))) * (N * (1,1))) + ((a * (N * (2,3))) * (N * (2,1)))) + ((b * (N * (3,3))) * (N * (3,1))) &
((N @) * (N1 * N)) * (3,2)
= (((a * (N * (1,3))) * (N * (1,2))) + ((a * (N * (2,3))) * (N * (2,2)))) + ((b * (N * (3,3))) * (N * (3,2))) &
((N @) * (N1 * N)) * (3,3)
= (((a * (N * (1,3))) * (N * (1,3))) + ((a * (N * (2,3))) * (N * (2,3)))) + ((b * (N * (3,3))) * (N * (3,3))) )
by BKMODEL1:23;
A169:
(
ra = ((na * na) + (nd * nd)) - (ng * ng) &
rb = ((na * nb) + (nd * ne)) - (ng * nh) &
rc = ((na * nc) + (nd * nf)) - (ng * ni) &
rb = ((na * nb) + (nd * ne)) - (ng * nh) &
re = ((nb * nb) + (ne * ne)) - (nh * nh) &
rf = ((nb * nc) + (ne * nf)) - (nh * ni) &
rc = ((na * nc) + (nd * nf)) - (ng * ni) &
rf = ((nb * nc) + (ne * nf)) - (nh * ni) &
ri = ((nc * nc) + (nf * nf)) - (ni * ni) )
by A166, A167, PASCAL:2, A168;
A170:
(((nb * na) + (nb * nc)) + (ne * nd)) + (ne * nf) = (nh * ng) + (nh * ni)
by A136;
(((- (nb * na)) + (nb * nc)) + (- (ne * nd))) + (ne * nf) = (- (nh * ng)) + (nh * ni)
by A81;
hence
(
rb = 0 &
rf = 0 &
ra = re )
by A170, A169, A22, A29, A35;
verum
end;
then A170:
M = symmetric_3 (ra,ra,(- ra),0,0,0)
by A12, A11, PASCAL:def 3;
A171:
ra <> 0
then A172:
(homography M) .: absolute = absolute
by A170, Th29;
take
N
; ( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )
thus
( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )
by A9, A171, A172, A170, A3, A4, A5, A6, BKMODEL1:93; verum