let M be Matrix of 3,REAL; for P being Element of absolute
for Q being Element of real_projective_plane
for u, v being non zero Element of (TOP-REAL 3)
for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds
SumAll (QuadraticForm (fq,M,fp)) = 0
let P be Element of absolute ; for Q being Element of real_projective_plane
for u, v being non zero Element of (TOP-REAL 3)
for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds
SumAll (QuadraticForm (fq,M,fp)) = 0
let Q be Element of real_projective_plane; for u, v being non zero Element of (TOP-REAL 3)
for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds
SumAll (QuadraticForm (fq,M,fp)) = 0
let u, v be non zero Element of (TOP-REAL 3); for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds
SumAll (QuadraticForm (fq,M,fp)) = 0
let fp, fq be FinSequence of REAL ; ( M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P implies SumAll (QuadraticForm (fq,M,fp)) = 0 )
assume that
A1:
M = symmetric_3 (1,1,(- 1),0,0,0)
and
A2:
P = Dir u
and
A3:
Q = Dir v
and
A4:
u = fp
and
A5:
v = fq
and
A6:
Q in tangent P
; SumAll (QuadraticForm (fq,M,fp)) = 0
consider p being Element of real_projective_plane such that
A7:
p = P
and
A8:
tangent P = Line (p,(pole_infty P))
by Def04;
A9:
p, pole_infty P,Q are_collinear
by A6, A8, COLLSP:11;
consider w being non zero Element of (TOP-REAL 3) such that
A10:
( P = Dir w & w . 3 = 1 & ((w . 1) ^2) + ((w . 2) ^2) = 1 & pole_infty P = Dir |[(- (w . 2)),(w . 1),0]| )
by Def03;
are_Prop w,u
by A2, A10, ANPROJ_1:22;
then consider aa being Real such that
A11:
aa <> 0
and
A12:
w = aa * u
by ANPROJ_1:1;
A13:
( w . 1 = aa * (u `1) & w . 2 = aa * (u `2) & w . 3 = aa * (u `3) )
then
( 1 * (w . 1) = aa * (u `1) & 1 * (w . 2) = aa * (u `2) & 1 = aa * (u `3) )
by A10;
then A14:
( (aa * (1 / aa)) * (w . 1) = aa * (u `1) & (aa * (1 / aa)) * (w . 2) = aa * (u `2) & (aa * (1 / aa)) * 1 = aa * (u `3) )
by A11, XCMPLX_1:106;
A16:
1 = (aa ^2) * (((u `1) * (u `1)) + ((u `2) * (u `2)))
by A13, A10;
A17:
( |[(- (w . 2)),(w . 1),0]| `1 = - (aa * (u `2)) & |[(- (w . 2)),(w . 1),0]| `2 = aa * (u `1) & |[(- (w . 2)),(w . 1),0]| `3 = 0 )
by A13, EUCLID_5:2;
not |[(- (w . 2)),(w . 1),0]| is zero
by BKMODEL1:91, A10;
then 0 =
|{u,|[(- (w . 2)),(w . 1),0]|,v}|
by A7, A10, A2, A3, A9, BKMODEL1:1
.=
(((((((u `1) * (|[(- (w . 2)),(w . 1),0]| `2)) * (v `3)) - (((u `3) * (|[(- (w . 2)),(w . 1),0]| `2)) * (v `1))) - (((u `1) * (|[(- (w . 2)),(w . 1),0]| `3)) * (v `2))) + (((u `2) * (|[(- (w . 2)),(w . 1),0]| `3)) * (v `1))) - (((u `2) * (|[(- (w . 2)),(w . 1),0]| `1)) * (v `3))) + (((u `3) * (|[(- (w . 2)),(w . 1),0]| `1)) * (v `2))
by ANPROJ_8:27
.=
aa * ((((((u `1) * (u `1)) * (v `3)) - (((u `1) * (u `3)) * (v `1))) + (((u `2) * (u `2)) * (v `3))) - (((u `2) * (u `3)) * (v `2)))
by A17
;
then 0 =
((v `3) * (((u `1) * (u `1)) + ((u `2) * (u `2)))) - ((u `3) * (((u `1) * (v `1)) + ((u `2) * (v `2))))
by A11
.=
((v `3) * (1 / (aa ^2))) - ((u `3) * (((u `1) * (v `1)) + ((u `2) * (v `2))))
by A16, XCMPLX_1:73
.=
((v `3) * (1 / (aa ^2))) - ((1 / aa) * (((u `1) * (v `1)) + ((u `2) * (v `2))))
by A14, A11, XCMPLX_1:5
.=
((v `3) * ((1 / aa) * (1 / aa))) - ((1 / aa) * (((u `1) * (v `1)) + ((u `2) * (v `2))))
by XCMPLX_1:102
.=
(1 / aa) * (((v `3) * (1 / aa)) - (((u `1) * (v `1)) + ((u `2) * (v `2))))
;
then A18:
((v `3) * (1 / aa)) - (((u `1) * (v `1)) + ((u `2) * (v `2))) = 0
by A11;
A19:
( len fp = width M & len fq = len M & len fp = len M & len fq = width M & len fp > 0 & len fq > 0 )
then A20: SumAll (QuadraticForm (fq,M,fp)) =
|((fq * M),fp)|
by MATRPROB:46
.=
|(fq,(M * fp))|
by A19, MATRPROB:47
;
A21:
M * fp = Col ((M * (ColVec2Mx fp)),1)
by MATRIXR1:def 11;
A22:
fp is Element of REAL 3
by A4, EUCLID:22;
then A23:
len fp = 3
by EUCLID_8:50;
reconsider fa = 1, fb = - 1, z = 0 as Element of F_Real by XREAL_0:def 1;
A24:
M = <*<*fa,z,z*>,<*z,fa,z*>,<*z,z,fb*>*>
by A1, PASCAL:def 3;
reconsider fp1 = fp . 1, fp2 = fp . 2, fp3 = fp . 3 as Element of F_Real by XREAL_0:def 1;
A25: ColVec2Mx fp =
MXR2MXF (ColVec2Mx fp)
by MATRIXR1:def 1
.=
<*fp*> @
by A22, ANPROJ_8:72
.=
F2M fp
by A22, ANPROJ_8:88, EUCLID_8:50
.=
<*<*fp1*>,<*fp2*>,<*fp3*>*>
by A23, ANPROJ_8:def 1
;
reconsider M1 = M as Matrix of 3,3,F_Real ;
reconsider M2 = <*<*fp1*>,<*fp2*>,<*fp3*>*> as Matrix of 3,1,F_Real by ANPROJ_8:4;
A26:
for n, k, m being Nat
for A being Matrix of n,k,F_Real
for B being Matrix of width A,m,F_Real holds A * B is Matrix of len A, width B,F_Real
;
A27:
( len M1 = 3 & width M2 = 1 )
by MATRIX_0:23;
width M1 = 3
by MATRIX_0:23;
then A28:
M1 * M2 is Matrix of 3,1,F_Real
by A26, A27;
A29:
M * (ColVec2Mx fp) = M1 * M2
by A25, ANPROJ_8:17;
M * (ColVec2Mx fp) =
M1 * M2
by A25, ANPROJ_8:17
.=
<*<*(((fa * fp1) + (z * fp2)) + (z * fp3))*>,<*(((z * fp1) + (fa * fp2)) + (z * fp3))*>,<*(((z * fp1) + (z * fp2)) + (fb * fp3))*>*>
by A24, ANPROJ_9:7
;
then SumAll (QuadraticForm (fq,M,fp)) =
|(v,|[fp1,fp2,(- fp3)]|)|
by A5, A20, A21, A28, A29, ANPROJ_8:5
.=
(((v `1) * (|[fp1,fp2,(- fp3)]| `1)) + ((v `2) * (|[fp1,fp2,(- fp3)]| `2))) + ((v `3) * (|[fp1,fp2,(- fp3)]| `3))
by EUCLID_5:29
.=
(((v `1) * fp1) + ((v `2) * (|[fp1,fp2,(- fp3)]| `2))) + ((v `3) * (|[fp1,fp2,(- fp3)]| `3))
by EUCLID_5:2
.=
(((v `1) * fp1) + ((v `2) * fp2)) + ((v `3) * (|[fp1,fp2,(- fp3)]| `3))
by EUCLID_5:2
.=
(((v `1) * fp1) + ((v `2) * fp2)) + ((v `3) * (- fp3))
by EUCLID_5:2
.=
(((v `1) * (u . 1)) + ((v `2) * (u . 2))) - ((v `3) * (u . 3))
by A4
.=
(((v `1) * (u `1)) + ((v `2) * (u . 2))) - ((v `3) * (u . 3))
by EUCLID_5:def 1
.=
(((v `1) * (u `1)) + ((v `2) * (u `2))) - ((v `3) * (u . 3))
by EUCLID_5:def 2
.=
(((v `1) * (u `1)) + ((v `2) * (u `2))) - ((v `3) * (u `3))
by EUCLID_5:def 3
.=
0
by A18, A14, A11, XCMPLX_1:5
;
hence
SumAll (QuadraticForm (fq,M,fp)) = 0
; verum