parsp_2.miz
begin
Lm1: for F be
add-associative
right_zeroed
right_complementable non
empty
addLoopStr, a,b be
Element of F holds (a
- b)
= (
0. F) implies a
= b
proof
let F be
add-associative
right_zeroed
right_complementable non
empty
addLoopStr, a,b be
Element of F;
assume (a
- b)
= (
0. F);
then (a
+ (
- b))
= (
0. F) by
RLVECT_1:def 11;
then a
= (
- (
- b)) by
RLVECT_1: 6;
hence thesis by
RLVECT_1: 17;
end;
Lm2: for F be
add-associative
right_zeroed
right_complementable non
empty
addLoopStr, x,y be
Element of F holds ((x
+ (
- y))
= (
0. F) iff x
= y) & ((x
- y)
= (
0. F) iff x
= y)
proof
let F be
add-associative
right_zeroed
right_complementable non
empty
addLoopStr, x,y be
Element of F;
A1: (x
+ (
- y))
= (
0. F) implies x
= y
proof
assume (x
+ (
- y))
= (
0. F);
then (x
+ ((
- y)
+ y))
= ((
0. F)
+ y) by
RLVECT_1:def 3;
then (x
+ (
0. F))
= ((
0. F)
+ y) by
RLVECT_1: 5;
then x
= ((
0. F)
+ y) by
RLVECT_1: 4;
hence thesis by
RLVECT_1: 4;
end;
A2: (x
- y)
= (
0. F) implies x
= y
proof
assume (x
- y)
= (
0. F);
then ((x
+ (
- y))
+ y)
= ((
0. F)
+ y) by
RLVECT_1:def 11;
then (x
+ ((
- y)
+ y))
= ((
0. F)
+ y) by
RLVECT_1:def 3;
then (x
+ (
0. F))
= ((
0. F)
+ y) by
RLVECT_1: 5;
then x
= ((
0. F)
+ y) by
RLVECT_1: 4;
hence thesis by
RLVECT_1: 4;
end;
x
= y implies (x
- y)
= (
0. F)
proof
assume x
= y;
then (x
- y)
= (y
+ (
- y)) by
RLVECT_1:def 11;
hence thesis by
RLVECT_1: 5;
end;
hence thesis by
A1,
A2,
RLVECT_1: 5;
end;
reserve F for
Field;
theorem ::
PARSP_2:1
Th1: (
MPS F) is
ParSp
proof
for a,b,c,d,p,q,r,s be
Element of (
MPS F) holds (a,b)
'||' (b,a) & (a,b)
'||' (c,c) & ((a,b)
'||' (p,q) & (a,b)
'||' (r,s) implies (p,q)
'||' (r,s) or a
= b) & ((a,b)
'||' (a,c) implies (b,a)
'||' (b,c)) & ex x be
Element of (
MPS F) st (a,b)
'||' (c,x) & (a,c)
'||' (b,x) by
PARSP_1: 13,
PARSP_1: 14,
PARSP_1: 15,
PARSP_1: 16,
PARSP_1: 17;
hence thesis by
PARSP_1:def 12;
end;
reserve a,b,c,d,p,q,r for
Element of (
MPS F);
reserve e,f,g,h,i,j,k,l,m,n,o,w for
Element of
[:the
carrier of F, the
carrier of F, the
carrier of F:];
reserve K,L,M,N,R,S for
Element of F;
Lm3: ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (
0. F) & ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) & ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) iff (ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F)
proof
A1: ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (
0. F) & ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) & ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) implies (ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F)
proof
assume that
A2: ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (
0. F) and
A3: ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) and
A4: ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F);
now
A5:
now
assume
A6: ((e
`3_3 )
- (f
`3_3 ))
<> (
0. F);
A7: ((((g
`3_3 )
- (h
`3_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
" ))
* ((e
`3_3 )
- (f
`3_3 )))
= (((g
`3_3 )
- (h
`3_3 ))
* ((((e
`3_3 )
- (f
`3_3 ))
" )
* ((e
`3_3 )
- (f
`3_3 )))) by
GROUP_1:def 3
.= (((g
`3_3 )
- (h
`3_3 ))
* (
1_ F)) by
A6,
VECTSP_1:def 10
.= ((g
`3_3 )
- (h
`3_3 ));
A8: ((((g
`3_3 )
- (h
`3_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
" ))
* ((e
`2_3 )
- (f
`2_3 )))
= ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
* (((e
`3_3 )
- (f
`3_3 ))
" )) by
GROUP_1:def 3
.= ((((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 )))
* (((e
`3_3 )
- (f
`3_3 ))
" )) by
A4,
Lm1
.= (((g
`2_3 )
- (h
`2_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
" ))) by
GROUP_1:def 3
.= (((g
`2_3 )
- (h
`2_3 ))
* (
1_ F)) by
A6,
VECTSP_1:def 10
.= ((g
`2_3 )
- (h
`2_3 ));
((((g
`3_3 )
- (h
`3_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
" ))
* ((e
`1_3 )
- (f
`1_3 )))
= ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
* (((e
`3_3 )
- (f
`3_3 ))
" )) by
GROUP_1:def 3
.= ((((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 )))
* (((e
`3_3 )
- (f
`3_3 ))
" )) by
A3,
Lm1
.= (((g
`1_3 )
- (h
`1_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
* (((e
`3_3 )
- (f
`3_3 ))
" ))) by
GROUP_1:def 3
.= (((g
`1_3 )
- (h
`1_3 ))
* (
1_ F)) by
A6,
VECTSP_1:def 10
.= ((g
`1_3 )
- (h
`1_3 ));
hence thesis by
A8,
A7;
end;
A9:
now
assume
A10: ((e
`2_3 )
- (f
`2_3 ))
<> (
0. F);
A11: ((((g
`2_3 )
- (h
`2_3 ))
* (((e
`2_3 )
- (f
`2_3 ))
" ))
* ((e
`2_3 )
- (f
`2_3 )))
= (((g
`2_3 )
- (h
`2_3 ))
* ((((e
`2_3 )
- (f
`2_3 ))
" )
* ((e
`2_3 )
- (f
`2_3 )))) by
GROUP_1:def 3
.= (((g
`2_3 )
- (h
`2_3 ))
* (
1_ F)) by
A10,
VECTSP_1:def 10
.= ((g
`2_3 )
- (h
`2_3 ));
A12: ((((g
`2_3 )
- (h
`2_3 ))
* (((e
`2_3 )
- (f
`2_3 ))
" ))
* ((e
`3_3 )
- (f
`3_3 )))
= ((((e
`2_3 )
- (f
`2_3 ))
" )
* (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 )))) by
GROUP_1:def 3
.= ((((e
`2_3 )
- (f
`2_3 ))
" )
* (((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))) by
A4,
Lm1
.= (((((e
`2_3 )
- (f
`2_3 ))
" )
* ((e
`2_3 )
- (f
`2_3 )))
* ((g
`3_3 )
- (h
`3_3 ))) by
GROUP_1:def 3
.= (((g
`3_3 )
- (h
`3_3 ))
* (
1_ F)) by
A10,
VECTSP_1:def 10
.= ((g
`3_3 )
- (h
`3_3 ));
((((g
`2_3 )
- (h
`2_3 ))
* (((e
`2_3 )
- (f
`2_3 ))
" ))
* ((e
`1_3 )
- (f
`1_3 )))
= ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
* (((e
`2_3 )
- (f
`2_3 ))
" )) by
GROUP_1:def 3
.= ((((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 )))
* (((e
`2_3 )
- (f
`2_3 ))
" )) by
A2,
Lm1
.= (((g
`1_3 )
- (h
`1_3 ))
* (((e
`2_3 )
- (f
`2_3 ))
* (((e
`2_3 )
- (f
`2_3 ))
" ))) by
GROUP_1:def 3
.= (((g
`1_3 )
- (h
`1_3 ))
* (
1_ F)) by
A10,
VECTSP_1:def 10
.= ((g
`1_3 )
- (h
`1_3 ));
hence thesis by
A11,
A12;
end;
now
assume
A13: ((e
`1_3 )
- (f
`1_3 ))
<> (
0. F);
A14: ((((g
`1_3 )
- (h
`1_3 ))
* (((e
`1_3 )
- (f
`1_3 ))
" ))
* ((e
`1_3 )
- (f
`1_3 )))
= (((g
`1_3 )
- (h
`1_3 ))
* ((((e
`1_3 )
- (f
`1_3 ))
" )
* ((e
`1_3 )
- (f
`1_3 )))) by
GROUP_1:def 3
.= (((g
`1_3 )
- (h
`1_3 ))
* (
1_ F)) by
A13,
VECTSP_1:def 10
.= ((g
`1_3 )
- (h
`1_3 ));
A15: ((((g
`1_3 )
- (h
`1_3 ))
* (((e
`1_3 )
- (f
`1_3 ))
" ))
* ((e
`3_3 )
- (f
`3_3 )))
= ((((e
`1_3 )
- (f
`1_3 ))
" )
* (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 )))) by
GROUP_1:def 3
.= ((((e
`1_3 )
- (f
`1_3 ))
" )
* (((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))) by
A3,
Lm1
.= (((((e
`1_3 )
- (f
`1_3 ))
" )
* ((e
`1_3 )
- (f
`1_3 )))
* ((g
`3_3 )
- (h
`3_3 ))) by
GROUP_1:def 3
.= (((g
`3_3 )
- (h
`3_3 ))
* (
1_ F)) by
A13,
VECTSP_1:def 10
.= ((g
`3_3 )
- (h
`3_3 ));
((((g
`1_3 )
- (h
`1_3 ))
* (((e
`1_3 )
- (f
`1_3 ))
" ))
* ((e
`2_3 )
- (f
`2_3 )))
= ((((e
`1_3 )
- (f
`1_3 ))
" )
* (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 )))) by
GROUP_1:def 3
.= ((((e
`1_3 )
- (f
`1_3 ))
" )
* (((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))) by
A2,
Lm1
.= (((((e
`1_3 )
- (f
`1_3 ))
" )
* ((e
`1_3 )
- (f
`1_3 )))
* ((g
`2_3 )
- (h
`2_3 ))) by
GROUP_1:def 3
.= (((g
`2_3 )
- (h
`2_3 ))
* (
1_ F)) by
A13,
VECTSP_1:def 10
.= ((g
`2_3 )
- (h
`2_3 ));
hence thesis by
A14,
A15;
end;
hence thesis by
A9,
A5;
end;
hence thesis;
end;
(ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F) implies ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (
0. F) & ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) & ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F)
proof
A16:
now
given K such that
A17: (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) and
A18: (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ));
A19: ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`3_3 )
- (f
`3_3 )))
- ((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`3_3 )
- (f
`3_3 )))) by
A18,
GROUP_1:def 3;
((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`2_3 )
- (f
`2_3 )))
- ((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`2_3 )
- (f
`2_3 )))) & ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`3_3 )
- (f
`3_3 )))
- ((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`3_3 )
- (f
`3_3 )))) by
A17,
A18,
GROUP_1:def 3;
hence thesis by
A19,
RLVECT_1: 15;
end;
A20: ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F) implies thesis by
RLVECT_1: 15;
assume (ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F);
hence thesis by
A20,
A16;
end;
hence thesis by
A1;
end;
theorem ::
PARSP_2:2
Th2: (a,b)
'||' (c,d) iff ex e, f, g, h st
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] & ((ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F))
proof
A1: (a,b)
'||' (c,d) implies ex e, f, g, h st
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] & ((ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F))
proof
assume (a,b)
'||' (c,d);
then
consider e, f, g, h such that
A2:
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] and
A3: ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (
0. F) & ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) & ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) by
PARSP_1: 12;
(ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F) by
A3,
Lm3;
hence thesis by
A2;
end;
(ex e, f, g, h st
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] & ((ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or (((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F)))) implies (a,b)
'||' (c,d)
proof
given e, f, g, h such that
A4:
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] and
A5: (ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F);
A6: ((((e
`2_3 )
- (f
`2_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`2_3 )
- (h
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) by
A5,
Lm3;
((((e
`1_3 )
- (f
`1_3 ))
* ((g
`2_3 )
- (h
`2_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= (
0. F) & ((((e
`1_3 )
- (f
`1_3 ))
* ((g
`3_3 )
- (h
`3_3 )))
- (((g
`1_3 )
- (h
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
= (
0. F) by
A5,
Lm3;
hence thesis by
A4,
A6,
PARSP_1: 12;
end;
hence thesis by
A1;
end;
theorem ::
PARSP_2:3
Th3: not (a,b)
'||' (a,c) &
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]] implies e
<> f & e
<> g & f
<> g
proof
assume
A1: ( not (a,b)
'||' (a,c)) &
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]];
then ((
0. F)
* ((e
`1_3 )
- (f
`1_3 )))
<> ((e
`1_3 )
- (g
`1_3 )) or ((
0. F)
* ((e
`2_3 )
- (f
`2_3 )))
<> ((e
`2_3 )
- (g
`2_3 )) or ((
0. F)
* ((e
`3_3 )
- (f
`3_3 )))
<> ((e
`3_3 )
- (g
`3_3 )) by
Th2;
then
A2: (
0. F)
<> ((e
`1_3 )
- (g
`1_3 )) or (
0. F)
<> ((e
`2_3 )
- (g
`2_3 )) or (
0. F)
<> ((e
`3_3 )
- (g
`3_3 ));
A3: f
<> g
proof
assume
A4: not thesis;
(((e
`1_3 )
- (f
`1_3 ))
* (
1_ F))
<> ((e
`1_3 )
- (g
`1_3 )) or (((e
`2_3 )
- (f
`2_3 ))
* (
1_ F))
<> ((e
`2_3 )
- (g
`2_3 )) or (((e
`3_3 )
- (f
`3_3 ))
* (
1_ F))
<> ((e
`3_3 )
- (g
`3_3 )) by
A1,
Th2;
hence contradiction by
A4;
end;
((e
`1_3 )
- (f
`1_3 ))
<> (
0. F) or ((e
`2_3 )
- (f
`2_3 ))
<> (
0. F) or ((e
`3_3 )
- (f
`3_3 ))
<> (
0. F) by
A1,
Th2;
hence thesis by
A2,
A3,
RLVECT_1: 15;
end;
theorem ::
PARSP_2:4
Th4: not (a,b)
'||' (a,c) &
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]] & (K
* ((e
`1_3 )
- (f
`1_3 )))
= (L
* ((e
`1_3 )
- (g
`1_3 ))) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= (L
* ((e
`2_3 )
- (g
`2_3 ))) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= (L
* ((e
`3_3 )
- (g
`3_3 ))) implies K
= (
0. F) & L
= (
0. F)
proof
assume that
A1: ( not (a,b)
'||' (a,c)) &
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]] and
A2: (K
* ((e
`1_3 )
- (f
`1_3 )))
= (L
* ((e
`1_3 )
- (g
`1_3 ))) and
A3: (K
* ((e
`2_3 )
- (f
`2_3 )))
= (L
* ((e
`2_3 )
- (g
`2_3 ))) and
A4: (K
* ((e
`3_3 )
- (f
`3_3 )))
= (L
* ((e
`3_3 )
- (g
`3_3 )));
e
=
[(e
`1_3 ), (e
`2_3 ), (e
`3_3 )] & g
=
[(g
`1_3 ), (g
`2_3 ), (g
`3_3 )];
then (e
`1_3 )
<> (g
`1_3 ) or (e
`2_3 )
<> (g
`2_3 ) or (e
`3_3 )
<> (g
`3_3 ) by
A1,
Th3;
then
A5: ((e
`1_3 )
- (g
`1_3 ))
<> (
0. F) or ((e
`2_3 )
- (g
`2_3 ))
<> (
0. F) or ((e
`3_3 )
- (g
`3_3 ))
<> (
0. F) by
Lm2;
((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`2_3 )
- (g
`2_3 )))
= (L
* (((e
`1_3 )
- (g
`1_3 ))
* ((e
`2_3 )
- (g
`2_3 )))) & ((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`1_3 )
- (g
`1_3 )))
= (L
* (((e
`2_3 )
- (g
`2_3 ))
* ((e
`1_3 )
- (g
`1_3 )))) by
A2,
A3,
GROUP_1:def 3;
then (((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`2_3 )
- (g
`2_3 )))
- ((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`1_3 )
- (g
`1_3 ))))
= (
0. F) by
RLVECT_1: 15;
then ((K
* (((e
`1_3 )
- (f
`1_3 ))
* ((e
`2_3 )
- (g
`2_3 ))))
- ((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`1_3 )
- (g
`1_3 ))))
= (
0. F) by
GROUP_1:def 3;
then ((K
* (((e
`1_3 )
- (f
`1_3 ))
* ((e
`2_3 )
- (g
`2_3 ))))
- (K
* (((e
`2_3 )
- (f
`2_3 ))
* ((e
`1_3 )
- (g
`1_3 )))))
= (
0. F) by
GROUP_1:def 3;
then
A6: (K
* ((((e
`1_3 )
- (f
`1_3 ))
* ((e
`2_3 )
- (g
`2_3 )))
- (((e
`1_3 )
- (g
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 )))))
= (
0. F) by
VECTSP_1: 11;
((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`3_3 )
- (g
`3_3 )))
= (L
* (((e
`1_3 )
- (g
`1_3 ))
* ((e
`3_3 )
- (g
`3_3 )))) & ((K
* ((e
`3_3 )
- (f
`3_3 )))
* ((e
`1_3 )
- (g
`1_3 )))
= (L
* (((e
`3_3 )
- (g
`3_3 ))
* ((e
`1_3 )
- (g
`1_3 )))) by
A2,
A4,
GROUP_1:def 3;
then (((K
* ((e
`1_3 )
- (f
`1_3 )))
* ((e
`3_3 )
- (g
`3_3 )))
- ((K
* ((e
`3_3 )
- (f
`3_3 )))
* ((e
`1_3 )
- (g
`1_3 ))))
= (
0. F) by
RLVECT_1: 15;
then ((K
* (((e
`1_3 )
- (f
`1_3 ))
* ((e
`3_3 )
- (g
`3_3 ))))
- ((K
* ((e
`3_3 )
- (f
`3_3 )))
* ((e
`1_3 )
- (g
`1_3 ))))
= (
0. F) by
GROUP_1:def 3;
then ((K
* (((e
`1_3 )
- (f
`1_3 ))
* ((e
`3_3 )
- (g
`3_3 ))))
- (K
* (((e
`3_3 )
- (f
`3_3 ))
* ((e
`1_3 )
- (g
`1_3 )))))
= (
0. F) by
GROUP_1:def 3;
then
A7: (K
* ((((e
`1_3 )
- (f
`1_3 ))
* ((e
`3_3 )
- (g
`3_3 )))
- (((e
`1_3 )
- (g
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 )))))
= (
0. F) by
VECTSP_1: 11;
((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`3_3 )
- (g
`3_3 )))
= (L
* (((e
`2_3 )
- (g
`2_3 ))
* ((e
`3_3 )
- (g
`3_3 )))) & ((K
* ((e
`3_3 )
- (f
`3_3 )))
* ((e
`2_3 )
- (g
`2_3 )))
= (L
* (((e
`3_3 )
- (g
`3_3 ))
* ((e
`2_3 )
- (g
`2_3 )))) by
A3,
A4,
GROUP_1:def 3;
then (((K
* ((e
`2_3 )
- (f
`2_3 )))
* ((e
`3_3 )
- (g
`3_3 )))
- ((K
* ((e
`3_3 )
- (f
`3_3 )))
* ((e
`2_3 )
- (g
`2_3 ))))
= (
0. F) by
RLVECT_1: 15;
then ((K
* (((e
`2_3 )
- (f
`2_3 ))
* ((e
`3_3 )
- (g
`3_3 ))))
- ((K
* ((e
`3_3 )
- (f
`3_3 )))
* ((e
`2_3 )
- (g
`2_3 ))))
= (
0. F) by
GROUP_1:def 3;
then ((K
* (((e
`2_3 )
- (f
`2_3 ))
* ((e
`3_3 )
- (g
`3_3 ))))
- (K
* (((e
`3_3 )
- (f
`3_3 ))
* ((e
`2_3 )
- (g
`2_3 )))))
= (
0. F) by
GROUP_1:def 3;
then
A8: (K
* ((((e
`2_3 )
- (f
`2_3 ))
* ((e
`3_3 )
- (g
`3_3 )))
- (((e
`2_3 )
- (g
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 )))))
= (
0. F) by
VECTSP_1: 11;
A9: ((((e
`1_3 )
- (f
`1_3 ))
* ((e
`2_3 )
- (g
`2_3 )))
- (((e
`1_3 )
- (g
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
<> (
0. F) or ((((e
`2_3 )
- (f
`2_3 ))
* ((e
`3_3 )
- (g
`3_3 )))
- (((e
`2_3 )
- (g
`2_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
<> (
0. F) or ((((e
`1_3 )
- (f
`1_3 ))
* ((e
`3_3 )
- (g
`3_3 )))
- (((e
`1_3 )
- (g
`1_3 ))
* ((e
`3_3 )
- (f
`3_3 ))))
<> (
0. F) by
A1,
PARSP_1: 12;
then
A10: K
= (
0. F) by
A6,
A8,
A7,
VECTSP_1: 12;
then
A11: (
0. F)
= (L
* ((e
`3_3 )
- (g
`3_3 ))) by
A4;
(
0. F)
= (L
* ((e
`1_3 )
- (g
`1_3 ))) & (
0. F)
= (L
* ((e
`2_3 )
- (g
`2_3 ))) by
A2,
A3,
A10;
hence thesis by
A6,
A8,
A7,
A9,
A11,
A5,
VECTSP_1: 12;
end;
Lm4: for F be
add-associative
right_zeroed
right_complementable non
empty
addLoopStr, a,b,c be
Element of F holds ((b
+ a)
- (c
+ a))
= (b
- c)
proof
let F be
add-associative
right_zeroed
right_complementable non
empty
addLoopStr, a,b,c be
Element of F;
thus ((b
+ a)
- (c
+ a))
= ((b
+ a)
+ (
- (c
+ a))) by
RLVECT_1:def 11
.= ((b
+ a)
+ ((
- a)
+ (
- c))) by
RLVECT_1: 31
.= (((b
+ a)
+ (
- a))
+ (
- c)) by
RLVECT_1:def 3
.= ((b
+ (a
+ (
- a)))
+ (
- c)) by
RLVECT_1:def 3
.= ((b
+ (
0. F))
+ (
- c)) by
RLVECT_1:def 10
.= (b
+ (
- c)) by
RLVECT_1: 4
.= (b
- c) by
RLVECT_1:def 11;
end;
Lm5: ((K
- L)
- (R
- L))
= (K
- R)
proof
thus ((K
- L)
- (R
- L))
= ((K
+ (
- L))
- (R
- L)) by
RLVECT_1:def 11
.= (((
- L)
+ K)
- (R
+ (
- L))) by
RLVECT_1:def 11
.= (K
- R) by
Lm4;
end;
Lm6: ((K
* (N
- M))
- (L
* (N
- S)))
= (S
- M) implies ((K
+ (
- (
1_ F)))
* (N
- M))
= ((L
+ (
- (
1_ F)))
* (N
- S))
proof
assume ((K
* (N
- M))
- (L
* (N
- S)))
= (S
- M);
then ((K
* (N
- M))
- (L
* (N
- S)))
= (S
+ (
- M)) by
RLVECT_1:def 11
.= ((S
+ (
- M))
+ (
0. F)) by
RLVECT_1: 4
.= (((
- M)
+ S)
+ ((
- N)
+ N)) by
RLVECT_1: 5
.= (S
+ (((
- N)
+ N)
+ (
- M))) by
RLVECT_1:def 3
.= (S
+ ((
- N)
+ (N
+ (
- M)))) by
RLVECT_1:def 3
.= (S
+ ((
- N)
+ (N
- M))) by
RLVECT_1:def 11
.= ((S
+ (
- N))
+ (N
- M)) by
RLVECT_1:def 3
.= ((S
- N)
+ (N
- M)) by
RLVECT_1:def 11;
then (((K
* (N
- M))
+ (
- (L
* (N
- S))))
+ (L
* (N
- S)))
= (((S
- N)
+ (N
- M))
+ (L
* (N
- S))) by
RLVECT_1:def 11;
then ((K
* (N
- M))
+ ((
- (L
* (N
- S)))
+ (L
* (N
- S))))
= (((S
- N)
+ (N
- M))
+ (L
* (N
- S))) by
RLVECT_1:def 3;
then ((K
* (N
- M))
+ (
0. F))
= (((S
- N)
+ (N
- M))
+ (L
* (N
- S))) by
RLVECT_1: 5;
then (K
* (N
- M))
= (((S
- N)
+ (N
- M))
+ (L
* (N
- S))) by
RLVECT_1: 4
.= (((S
- N)
+ (L
* (N
- S)))
+ (N
- M)) by
RLVECT_1:def 3;
then ((K
* (N
- M))
+ (
- (N
- M)))
= (((S
- N)
+ (L
* (N
- S)))
+ ((N
- M)
+ (
- (N
- M)))) by
RLVECT_1:def 3
.= (((S
- N)
+ (L
* (N
- S)))
+ (
0. F)) by
RLVECT_1: 5
.= ((S
- N)
+ (L
* (N
- S))) by
RLVECT_1: 4
.= ((S
+ (
- N))
+ (L
* (N
- S))) by
RLVECT_1:def 11
.= ((L
* (N
- S))
+ (
- (N
- S))) by
RLVECT_1: 33;
then ((K
* (N
- M))
+ (
- ((
1_ F)
* (N
- M))))
= ((L
* (N
- S))
+ (
- (N
- S)));
then ((K
* (N
- M))
+ ((
- (
1_ F))
* (N
- M)))
= ((L
* (N
- S))
+ (
- (N
- S))) by
VECTSP_1: 9;
then ((K
+ (
- (
1_ F)))
* (N
- M))
= ((L
* (N
- S))
+ (
- (N
- S))) by
VECTSP_1:def 7
.= ((L
* (N
- S))
+ (
- ((
1_ F)
* (N
- S))))
.= ((L
* (N
- S))
+ ((
- (
1_ F))
* (N
- S))) by
VECTSP_1: 9;
hence thesis by
VECTSP_1:def 7;
end;
Lm7: (K
- L)
= (N
- M) implies M
= ((L
+ N)
- K)
proof
assume (K
- L)
= (N
- M);
then (M
+ (K
+ (
- L)))
= (M
+ (N
- M)) by
RLVECT_1:def 11;
then (M
+ (K
+ (
- L)))
= (M
+ (N
+ (
- M))) by
RLVECT_1:def 11;
then ((M
+ K)
+ (
- L))
= (M
+ (N
+ (
- M))) by
RLVECT_1:def 3;
then ((M
+ K)
+ (
- L))
= ((M
+ N)
+ (
- M)) by
RLVECT_1:def 3;
then ((M
+ K)
- L)
= ((N
+ M)
+ (
- M)) by
RLVECT_1:def 11;
then ((M
+ K)
- L)
= (N
+ (M
+ (
- M))) by
RLVECT_1:def 3;
then ((M
+ K)
- L)
= (N
+ (
0. F)) by
RLVECT_1: 5;
then (((M
+ K)
- L)
+ L)
= (N
+ L) by
RLVECT_1: 4;
then (((M
+ K)
+ (
- L))
+ L)
= (N
+ L) by
RLVECT_1:def 11;
then ((M
+ K)
+ ((
- L)
+ L))
= (N
+ L) by
RLVECT_1:def 3;
then ((M
+ K)
+ (
0. F))
= (L
+ N) by
RLVECT_1: 5;
then ((M
+ K)
+ (
- K))
= ((L
+ N)
+ (
- K)) by
RLVECT_1: 4;
then ((M
+ K)
+ (
- K))
= ((L
+ N)
- K) by
RLVECT_1:def 11;
then (M
+ (K
+ (
- K)))
= ((L
+ N)
- K) by
RLVECT_1:def 3;
then (M
+ (
0. F))
= ((L
+ N)
- K) by
RLVECT_1: 5;
hence thesis by
RLVECT_1: 4;
end;
theorem ::
PARSP_2:5
Th5: not (a,b)
'||' (a,c) & (a,b)
'||' (c,d) & (a,c)
'||' (b,d) &
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] implies (h
`1_3 )
= (((f
`1_3 )
+ (g
`1_3 ))
- (e
`1_3 )) & (h
`2_3 )
= (((f
`2_3 )
+ (g
`2_3 ))
- (e
`2_3 )) & (h
`3_3 )
= (((f
`3_3 )
+ (g
`3_3 ))
- (e
`3_3 ))
proof
assume that
A1: not (a,b)
'||' (a,c) and
A2: (a,b)
'||' (c,d) and
A3: (a,c)
'||' (b,d) and
A4:
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]];
consider m, n, o, w such that
A6:
[
[a, c],
[b, d]]
=
[
[m, n],
[o, w]] and
A7: (ex L st (L
* ((m
`1_3 )
- (n
`1_3 )))
= ((o
`1_3 )
- (w
`1_3 )) & (L
* ((m
`2_3 )
- (n
`2_3 )))
= ((o
`2_3 )
- (w
`2_3 )) & (L
* ((m
`3_3 )
- (n
`3_3 )))
= ((o
`3_3 )
- (w
`3_3 ))) or ((m
`1_3 )
- (n
`1_3 ))
= (
0. F) & ((m
`2_3 )
- (n
`2_3 ))
= (
0. F) & ((m
`3_3 )
- (n
`3_3 ))
= (
0. F) by
A3,
Th2;
A8: b
= f by
A4,
MCART_1: 93;
then
A9: o
= f by
A6,
MCART_1: 93;
d
= h by
A4,
MCART_1: 93;
then
A10: w
= h by
A6,
MCART_1: 93;
c
= g by
A4,
MCART_1: 93;
then
A11: n
= g by
A6,
MCART_1: 93;
A12: a
= e by
A4,
MCART_1: 93;
then
A13:
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]] by
A4,
A8,
MCART_1: 93;
consider i, j, k, l such that
A14:
[
[a, b],
[c, d]]
=
[
[i, j],
[k, l]] and
A15: (ex K st (K
* ((i
`1_3 )
- (j
`1_3 )))
= ((k
`1_3 )
- (l
`1_3 )) & (K
* ((i
`2_3 )
- (j
`2_3 )))
= ((k
`2_3 )
- (l
`2_3 )) & (K
* ((i
`3_3 )
- (j
`3_3 )))
= ((k
`3_3 )
- (l
`3_3 ))) or ((i
`1_3 )
- (j
`1_3 ))
= (
0. F) & ((i
`2_3 )
- (j
`2_3 ))
= (
0. F) & ((i
`3_3 )
- (j
`3_3 ))
= (
0. F) by
A2,
Th2;
A16: e
= i & f
= j by
A4,
A14,
MCART_1: 93;
A17: g
= k & h
= l by
A4,
A14,
MCART_1: 93;
A18: e
= m by
A12,
A6,
MCART_1: 93;
f
=
[(f
`1_3 ), (f
`2_3 ), (f
`3_3 )];
then (e
`1_3 )
<> (f
`1_3 ) or (e
`2_3 )
<> (f
`2_3 ) or (e
`3_3 )
<> (f
`3_3 ) by
A1,
A13,
Th3;
then
consider K such that
A19: (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) and
A20: (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) and
A21: (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 )) by
A15,
A16,
A17,
Lm2;
g
=
[(g
`1_3 ), (g
`2_3 ), (g
`3_3 )];
then (e
`1_3 )
<> (g
`1_3 ) or (e
`2_3 )
<> (g
`2_3 ) or (e
`3_3 )
<> (g
`3_3 ) by
A1,
A13,
Th3;
then
consider L such that
A22: (L
* ((e
`1_3 )
- (g
`1_3 )))
= ((f
`1_3 )
- (h
`1_3 )) and
A23: (L
* ((e
`2_3 )
- (g
`2_3 )))
= ((f
`2_3 )
- (h
`2_3 )) and
A24: (L
* ((e
`3_3 )
- (g
`3_3 )))
= ((f
`3_3 )
- (h
`3_3 )) by
A7,
A18,
A11,
A9,
A10,
Lm2;
((K
* ((e
`2_3 )
- (f
`2_3 )))
- (L
* ((e
`2_3 )
- (g
`2_3 ))))
= ((g
`2_3 )
- (f
`2_3 )) by
A20,
A23,
Lm5;
then
A25: ((K
+ (
- (
1_ F)))
* ((e
`2_3 )
- (f
`2_3 )))
= ((L
+ (
- (
1_ F)))
* ((e
`2_3 )
- (g
`2_3 ))) by
Lm6;
((K
* ((e
`3_3 )
- (f
`3_3 )))
- (L
* ((e
`3_3 )
- (g
`3_3 ))))
= ((g
`3_3 )
- (f
`3_3 )) by
A21,
A24,
Lm5;
then
A26: ((K
+ (
- (
1_ F)))
* ((e
`3_3 )
- (f
`3_3 )))
= ((L
+ (
- (
1_ F)))
* ((e
`3_3 )
- (g
`3_3 ))) by
Lm6;
((K
* ((e
`1_3 )
- (f
`1_3 )))
- (L
* ((e
`1_3 )
- (g
`1_3 ))))
= ((g
`1_3 )
- (f
`1_3 )) by
A19,
A22,
Lm5;
then ((K
+ (
- (
1_ F)))
* ((e
`1_3 )
- (f
`1_3 )))
= ((L
+ (
- (
1_ F)))
* ((e
`1_3 )
- (g
`1_3 ))) by
Lm6;
then
A27: (K
+ (
- (
1_ F)))
= (
0. F) by
A1,
A13,
A25,
A26,
Th4;
then (((e
`2_3 )
- (f
`2_3 ))
* (
1_ F))
= ((g
`2_3 )
- (h
`2_3 )) by
A20,
Lm2;
then
A28: ((e
`2_3 )
- (f
`2_3 ))
= ((g
`2_3 )
- (h
`2_3 ));
(((e
`3_3 )
- (f
`3_3 ))
* (
1_ F))
= ((g
`3_3 )
- (h
`3_3 )) by
A21,
A27,
Lm2;
then
A29: ((e
`3_3 )
- (f
`3_3 ))
= ((g
`3_3 )
- (h
`3_3 ));
(((e
`1_3 )
- (f
`1_3 ))
* (
1_ F))
= ((g
`1_3 )
- (h
`1_3 )) by
A19,
A27,
Lm2;
then ((e
`1_3 )
- (f
`1_3 ))
= ((g
`1_3 )
- (h
`1_3 ));
hence thesis by
A28,
A29,
Lm7;
end;
Lm8: ((L
* K)
- (L
* R))
= (R
+ K) implies ((L
- (
1_ F))
* K)
= ((L
+ (
1_ F))
* R)
proof
assume ((L
* K)
- (L
* R))
= (R
+ K);
then (((L
* K)
+ (
- (L
* R)))
+ (
- K))
= ((R
+ K)
+ (
- K)) by
RLVECT_1:def 11
.= (R
+ (K
+ (
- K))) by
RLVECT_1:def 3
.= (R
+ (
0. F)) by
RLVECT_1: 5
.= R by
RLVECT_1: 4;
then (((L
* K)
+ (
- K))
+ (
- (L
* R)))
= R by
RLVECT_1:def 3;
then (((L
* K)
+ (
- ((
1_ F)
* K)))
+ (
- (L
* R)))
= R;
then (((L
* K)
+ ((
- (
1_ F))
* K))
+ (
- (L
* R)))
= R by
VECTSP_1: 9;
then (((L
+ (
- (
1_ F)))
* K)
+ (
- (L
* R)))
= R by
VECTSP_1:def 7;
then ((((L
- (
1_ F))
* K)
+ (
- (L
* R)))
+ (L
* R))
= (R
+ (L
* R)) by
RLVECT_1:def 11;
then (((L
- (
1_ F))
* K)
+ ((
- (L
* R))
+ (L
* R)))
= (R
+ (L
* R)) by
RLVECT_1:def 3;
then (((L
- (
1_ F))
* K)
+ (
0. F))
= (R
+ (L
* R)) by
RLVECT_1: 5;
then ((L
- (
1_ F))
* K)
= ((L
* R)
+ R) by
RLVECT_1: 4
.= ((L
* R)
+ ((
1_ F)
* R));
hence thesis by
VECTSP_1:def 7;
end;
Lm9: (L
* (K
- N))
= (R
- S) & S
= ((K
+ N)
- R) implies ((L
- (
1_ F))
* (R
- N))
= ((L
+ (
1_ F))
* (R
- K))
proof
assume (L
* (K
- N))
= (R
- S) & S
= ((K
+ N)
- R);
then
A1: (L
* (K
- N))
= (R
+ (
- ((K
+ N)
- R))) by
RLVECT_1:def 11
.= (R
+ (R
+ (
- (K
+ N)))) by
RLVECT_1: 33
.= (R
+ (R
+ ((
- K)
+ (
- N)))) by
RLVECT_1: 31
.= (R
+ ((
- N)
+ (R
+ (
- K)))) by
RLVECT_1:def 3
.= ((R
+ (
- N))
+ (R
+ (
- K))) by
RLVECT_1:def 3
.= ((R
- N)
+ (R
+ (
- K))) by
RLVECT_1:def 11
.= ((R
- K)
+ (R
- N)) by
RLVECT_1:def 11;
((L
* (R
- N))
- (L
* (R
- K)))
= ((L
* (R
+ (
- N)))
- (L
* (R
- K))) by
RLVECT_1:def 11
.= ((L
* (R
+ (
- N)))
- (L
* (R
+ (
- K)))) by
RLVECT_1:def 11
.= ((L
* (R
+ (
- N)))
+ (
- (L
* (R
+ (
- K))))) by
RLVECT_1:def 11
.= (((L
* R)
+ (L
* (
- N)))
+ (
- (L
* (R
+ (
- K))))) by
VECTSP_1:def 7
.= (((L
* R)
+ (L
* (
- N)))
+ ((
- L)
* (R
+ (
- K)))) by
VECTSP_1: 9
.= (((L
* R)
+ (L
* (
- N)))
+ (((
- L)
* R)
+ ((
- L)
* (
- K)))) by
VECTSP_1:def 7
.= (((L
* R)
+ (L
* (
- N)))
+ (((
- L)
* R)
+ (L
* K))) by
VECTSP_1: 10
.= (((L
* (
- N))
+ (L
* R))
+ ((
- (L
* R))
+ (L
* K))) by
VECTSP_1: 9
.= ((((L
* (
- N))
+ (L
* R))
+ (
- (L
* R)))
+ (L
* K)) by
RLVECT_1:def 3
.= (((L
* (
- N))
+ ((L
* R)
+ (
- (L
* R))))
+ (L
* K)) by
RLVECT_1:def 3
.= (((L
* (
- N))
+ (
0. F))
+ (L
* K)) by
RLVECT_1: 5
.= ((L
* K)
+ (L
* (
- N))) by
RLVECT_1: 4
.= (L
* (K
+ (
- N))) by
VECTSP_1:def 7
.= (L
* (K
- N)) by
RLVECT_1:def 11;
hence thesis by
A1,
Lm8;
end;
Lm10: K
= ((L
+ M)
- N) & R
= ((L
+ S)
- N) implies ((
1_ F)
* (M
- S))
= (K
- R)
proof
assume that
A1: K
= ((L
+ M)
- N) and
A2: R
= ((L
+ S)
- N);
(
- R)
= (
- ((L
+ S)
+ (
- N))) by
A2,
RLVECT_1:def 11
.= ((
- (L
+ S))
+ (
- (
- N))) by
RLVECT_1: 31
.= ((
- (L
+ S))
+ N) by
RLVECT_1: 17
.= (((
- L)
+ (
- S))
+ N) by
RLVECT_1: 31;
then (K
- R)
= (((L
+ M)
- N)
+ (((
- L)
+ (
- S))
+ N)) by
A1,
RLVECT_1:def 11
.= (((M
+ L)
+ (
- N))
+ (((
- L)
+ (
- S))
+ N)) by
RLVECT_1:def 11
.= (((M
+ L)
+ (
- N))
+ ((
- S)
+ ((
- L)
+ N))) by
RLVECT_1:def 3
.= ((M
+ (L
+ (
- N)))
+ ((
- S)
+ ((
- L)
+ N))) by
RLVECT_1:def 3
.= ((M
+ (L
- N))
+ ((
- S)
+ ((
- L)
+ N))) by
RLVECT_1:def 11
.= ((M
+ (L
- N))
+ ((
- S)
+ ((
- L)
+ (
- (
- N))))) by
RLVECT_1: 17
.= ((M
+ (L
- N))
+ ((
- S)
+ (
- (L
+ (
- N))))) by
RLVECT_1: 31
.= ((M
+ (L
- N))
+ ((
- (L
- N))
+ (
- S))) by
RLVECT_1:def 11
.= (((M
+ (L
- N))
+ (
- (L
- N)))
+ (
- S)) by
RLVECT_1:def 3
.= ((M
+ ((L
- N)
+ (
- (L
- N))))
+ (
- S)) by
RLVECT_1:def 3
.= ((M
+ (
0. F))
+ (
- S)) by
RLVECT_1: 5
.= (M
+ (
- S)) by
RLVECT_1: 4
.= ((M
* (
1_ F))
+ (
- S))
.= ((M
* (
1_ F))
+ ((
- S)
* (
1_ F)))
.= ((M
+ (
- S))
* (
1_ F))
.= ((M
- S)
* (
1_ F)) by
RLVECT_1:def 11;
hence thesis;
end;
theorem ::
PARSP_2:6
Th6: ex a, b, c st not (a,b)
'||' (a,c)
proof
consider e,f,g be
Element of
[:the
carrier of F, the
carrier of F, the
carrier of F:] such that
A1: e
=
[(
1_ F), (
1_ F), (
0. F)] and
A2: f
=
[(
- (
0. F)), (
1_ F), (
0. F)] and
A3: g
=
[(
1_ F), (
- (
0. F)), (
0. F)];
A4: (f
`1_3 )
= (
- (
0. F)) & (f
`2_3 )
= (
1_ F) by
A2;
A5: (g
`1_3 )
= (
1_ F) & (g
`2_3 )
= (
- (
0. F)) by
A3;
the
carrier of (
MPS F)
=
[:the
carrier of F, the
carrier of F, the
carrier of F:] by
PARSP_1: 10;
then
consider a,b,c be
Element of (
MPS F) such that
A6:
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]];
take a, b, c;
(e
`1_3 )
= (
1_ F) & (e
`2_3 )
= (
1_ F) by
A1;
then
A7: ((((e
`1_3 )
- (f
`1_3 ))
* ((e
`2_3 )
- (g
`2_3 )))
- (((e
`1_3 )
- (g
`1_3 ))
* ((e
`2_3 )
- (f
`2_3 ))))
= ((((
1. F)
+ (
- (
- (
0. F))))
* ((
1. F)
- (
- (
0. F))))
- (((
1. F)
- (
1. F))
* ((
1. F)
- (
1. F)))) by
A4,
A5,
RLVECT_1:def 11
.= ((((
1. F)
+ (
- (
- (
0. F))))
* ((
1. F)
+ (
- (
- (
0. F)))))
- (((
1. F)
- (
1. F))
* ((
1. F)
- (
1. F)))) by
RLVECT_1:def 11
.= ((((
1. F)
+ (
0. F))
* ((
1. F)
+ (
- (
- (
0. F)))))
- (((
1. F)
- (
1. F))
* ((
1. F)
- (
1. F)))) by
RLVECT_1: 17
.= ((((
1. F)
+ (
0. F))
* ((
1. F)
+ (
0. F)))
- (((
1. F)
- (
1. F))
* ((
1. F)
- (
1. F)))) by
RLVECT_1: 17
.= (((
1. F)
* ((
1. F)
+ (
0. F)))
- (((
1. F)
- (
1. F))
* ((
1. F)
- (
1. F)))) by
RLVECT_1: 4
.= (((
1. F)
* (
1. F))
- (((
1. F)
- (
1. F))
* ((
1. F)
- (
1. F)))) by
RLVECT_1: 4
.= (((
1. F)
* (
1. F))
- ((
0. F)
* ((
1. F)
- (
1. F)))) by
RLVECT_1: 15
.= (((
1. F)
* (
1. F))
- (
0. F))
.= ((
1. F)
- (
0. F));
now
let e9,f9,g9,h9 be
Element of
[:the
carrier of F, the
carrier of F, the
carrier of F:];
assume
A8:
[
[e9, f9],
[g9, h9]]
=
[
[a, b],
[a, c]];
then
A9: g9
= e & h9
= g by
A6,
MCART_1: 93;
e9
= e & f9
= f by
A6,
A8,
MCART_1: 93;
hence ((((e9
`1_3 )
- (f9
`1_3 ))
* ((g9
`2_3 )
- (h9
`2_3 )))
- (((g9
`1_3 )
- (h9
`1_3 ))
* ((e9
`2_3 )
- (f9
`2_3 ))))
<> (
0. F) or ((((e9
`1_3 )
- (f9
`1_3 ))
* ((g9
`3_3 )
- (h9
`3_3 )))
- (((g9
`1_3 )
- (h9
`1_3 ))
* ((e9
`3_3 )
- (f9
`3_3 ))))
<> (
0. F) or ((((e9
`2_3 )
- (f9
`2_3 ))
* ((g9
`3_3 )
- (h9
`3_3 )))
- (((g9
`2_3 )
- (h9
`2_3 ))
* ((e9
`3_3 )
- (f9
`3_3 ))))
<> (
0. F) by
A7,
A9,
Lm2;
end;
hence thesis by
PARSP_1: 12;
end;
theorem ::
PARSP_2:7
Th7: ((
1_ F)
+ (
1_ F))
<> (
0. F) & (b,c)
'||' (a,d) & (a,b)
'||' (c,d) & (a,c)
'||' (b,d) implies (a,b)
'||' (a,c)
proof
assume that
A1: ((
1_ F)
+ (
1_ F))
<> (
0. F) and
A2: (b,c)
'||' (a,d) and
A3: (a,b)
'||' (c,d) and
A4: (a,c)
'||' (b,d);
assume
A5: not thesis;
consider i, j, k, l such that
A6:
[
[b, c],
[a, d]]
=
[
[i, j],
[k, l]] and
A7: (ex L st (L
* ((i
`1_3 )
- (j
`1_3 )))
= ((k
`1_3 )
- (l
`1_3 )) & (L
* ((i
`2_3 )
- (j
`2_3 )))
= ((k
`2_3 )
- (l
`2_3 )) & (L
* ((i
`3_3 )
- (j
`3_3 )))
= ((k
`3_3 )
- (l
`3_3 ))) or ((i
`1_3 )
- (j
`1_3 ))
= (
0. F) & ((i
`2_3 )
- (j
`2_3 ))
= (
0. F) & ((i
`3_3 )
- (j
`3_3 ))
= (
0. F) by
A2,
Th2;
A8: b
= i & c
= j by
A6,
MCART_1: 93;
A9: a
= k & d
= l by
A6,
MCART_1: 93;
consider e, f, g, h such that
A10:
[
[a, b],
[c, d]]
=
[
[e, f],
[g, h]] and (ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F) by
A3,
Th2;
A11: b
= f by
A10,
MCART_1: 93;
A12: d
= h by
A10,
MCART_1: 93;
A13: c
= g by
A10,
MCART_1: 93;
A14: a
= e by
A10,
MCART_1: 93;
then
A15:
[
[a, b],
[a, c]]
=
[
[e, f],
[e, g]] by
A10,
A11,
MCART_1: 93;
f
=
[(f
`1_3 ), (f
`2_3 ), (f
`3_3 )] & g
=
[(g
`1_3 ), (g
`2_3 ), (g
`3_3 )];
then (i
`1_3 )
<> (j
`1_3 ) or (i
`2_3 )
<> (j
`2_3 ) or (i
`3_3 )
<> (j
`3_3 ) by
A5,
A11,
A13,
A15,
A8,
Th3;
then
consider L such that
A16: (L
* ((f
`1_3 )
- (g
`1_3 )))
= ((e
`1_3 )
- (h
`1_3 )) and
A17: (L
* ((f
`2_3 )
- (g
`2_3 )))
= ((e
`2_3 )
- (h
`2_3 )) and
A18: (L
* ((f
`3_3 )
- (g
`3_3 )))
= ((e
`3_3 )
- (h
`3_3 )) by
A14,
A11,
A13,
A12,
A7,
A8,
A9,
Lm2;
(h
`2_3 )
= (((f
`2_3 )
+ (g
`2_3 ))
- (e
`2_3 )) by
A3,
A4,
A5,
A10,
Th5;
then
A19: ((L
- (
1_ F))
* ((e
`2_3 )
- (g
`2_3 )))
= ((L
+ (
1_ F))
* ((e
`2_3 )
- (f
`2_3 ))) by
A17,
Lm9;
(h
`3_3 )
= (((f
`3_3 )
+ (g
`3_3 ))
- (e
`3_3 )) by
A3,
A4,
A5,
A10,
Th5;
then
A20: ((L
- (
1_ F))
* ((e
`3_3 )
- (g
`3_3 )))
= ((L
+ (
1_ F))
* ((e
`3_3 )
- (f
`3_3 ))) by
A18,
Lm9;
(h
`1_3 )
= (((f
`1_3 )
+ (g
`1_3 ))
- (e
`1_3 )) by
A3,
A4,
A5,
A10,
Th5;
then ((L
- (
1_ F))
* ((e
`1_3 )
- (g
`1_3 )))
= ((L
+ (
1_ F))
* ((e
`1_3 )
- (f
`1_3 ))) by
A16,
Lm9;
then (L
+ (
1_ F))
= (
0. F) & (L
- (
1_ F))
= (
0. F) by
A5,
A15,
A19,
A20,
Th4;
then ((L
+ (
1_ F))
- (L
- (
1_ F)))
= ((
0. F)
+ (
- (
0. F))) by
RLVECT_1:def 11;
then ((L
+ (
1_ F))
- (L
- (
1_ F)))
= (
0. F) by
RLVECT_1: 5;
then ((L
+ (
1_ F))
+ (
- (L
- (
1_ F))))
= (
0. F) by
RLVECT_1:def 11;
then ((L
+ (
1_ F))
+ ((
1_ F)
+ (
- L)))
= (
0. F) by
RLVECT_1: 33;
then (((L
+ (
1_ F))
+ (
1_ F))
+ (
- L))
= (
0. F) by
RLVECT_1:def 3;
then ((((
1_ F)
+ (
1_ F))
+ L)
+ (
- L))
= (
0. F) by
RLVECT_1:def 3;
then (((
1_ F)
+ (
1_ F))
+ (L
+ (
- L)))
= (
0. F) by
RLVECT_1:def 3;
then (((
1_ F)
+ (
1_ F))
+ (
0. F))
= (
0. F) by
RLVECT_1: 5;
hence contradiction by
A1,
RLVECT_1: 4;
end;
theorem ::
PARSP_2:8
Th8: not (a,p)
'||' (a,b) & not (a,p)
'||' (a,c) & (a,p)
'||' (b,q) & (a,p)
'||' (c,r) & (a,b)
'||' (p,q) & (a,c)
'||' (p,r) implies (b,c)
'||' (q,r)
proof
assume that
A1: not (a,p)
'||' (a,b) and
A2: not (a,p)
'||' (a,c) and
A3: (a,p)
'||' (b,q) and
A4: (a,p)
'||' (c,r) and
A5: (a,b)
'||' (p,q) and
A6: (a,c)
'||' (p,r);
consider i, j, k, l such that
A7:
[
[a, p],
[c, r]]
=
[
[i, j],
[k, l]] and (ex L st (L
* ((i
`1_3 )
- (j
`1_3 )))
= ((k
`1_3 )
- (l
`1_3 )) & (L
* ((i
`2_3 )
- (j
`2_3 )))
= ((k
`2_3 )
- (l
`2_3 )) & (L
* ((i
`3_3 )
- (j
`3_3 )))
= ((k
`3_3 )
- (l
`3_3 ))) or ((i
`1_3 )
- (j
`1_3 ))
= (
0. F) & ((i
`2_3 )
- (j
`2_3 ))
= (
0. F) & ((i
`3_3 )
- (j
`3_3 ))
= (
0. F) by
A4,
Th2;
consider e, f, g, h such that
A8:
[
[a, b],
[p, q]]
=
[
[e, f],
[g, h]] and (ex K st (K
* ((e
`1_3 )
- (f
`1_3 )))
= ((g
`1_3 )
- (h
`1_3 )) & (K
* ((e
`2_3 )
- (f
`2_3 )))
= ((g
`2_3 )
- (h
`2_3 )) & (K
* ((e
`3_3 )
- (f
`3_3 )))
= ((g
`3_3 )
- (h
`3_3 ))) or ((e
`1_3 )
- (f
`1_3 ))
= (
0. F) & ((e
`2_3 )
- (f
`2_3 ))
= (
0. F) & ((e
`3_3 )
- (f
`3_3 ))
= (
0. F) by
A5,
Th2;
A9: a
= e & p
= g by
A8,
MCART_1: 93;
A10: c
= k by
A7,
MCART_1: 93;
then
A11:
[
[a, p],
[c, r]]
=
[
[e, g],
[k, l]] by
A9,
A7,
MCART_1: 93;
then
A12: (l
`1_3 )
= (((g
`1_3 )
+ (k
`1_3 ))
- (e
`1_3 )) by
A2,
A4,
A6,
Th5;
A13: b
= f by
A8,
MCART_1: 93;
then
A14:
[
[a, p],
[b, q]]
=
[
[e, g],
[f, h]] by
A8,
A9,
MCART_1: 93;
then (h
`1_3 )
= (((g
`1_3 )
+ (f
`1_3 ))
- (e
`1_3 )) by
A1,
A3,
A5,
Th5;
then
A15: ((
1_ F)
* ((f
`1_3 )
- (k
`1_3 )))
= ((h
`1_3 )
- (l
`1_3 )) by
A12,
Lm10;
A16: (l
`3_3 )
= (((g
`3_3 )
+ (k
`3_3 ))
- (e
`3_3 )) by
A2,
A4,
A6,
A11,
Th5;
A17: (l
`2_3 )
= (((g
`2_3 )
+ (k
`2_3 ))
- (e
`2_3 )) by
A2,
A4,
A6,
A11,
Th5;
(h
`3_3 )
= (((g
`3_3 )
+ (f
`3_3 ))
- (e
`3_3 )) by
A1,
A3,
A5,
A14,
Th5;
then
A18: ((
1_ F)
* ((f
`3_3 )
- (k
`3_3 )))
= ((h
`3_3 )
- (l
`3_3 )) by
A16,
Lm10;
(h
`2_3 )
= (((g
`2_3 )
+ (f
`2_3 ))
- (e
`2_3 )) by
A1,
A3,
A5,
A14,
Th5;
then
A19: ((
1_ F)
* ((f
`2_3 )
- (k
`2_3 )))
= ((h
`2_3 )
- (l
`2_3 )) by
A17,
Lm10;
q
= h by
A8,
MCART_1: 93;
then
[
[b, c],
[q, r]]
=
[
[f, k],
[h, l]] by
A13,
A7,
A10,
MCART_1: 93;
hence thesis by
A15,
A19,
A18,
Th2;
end;
definition
let IT be
ParSp;
::
PARSP_2:def1
attr IT is
FanodesSp-like means
:
Def1: (ex a,b,c be
Element of IT st not (a,b)
'||' (a,c)) & (for a,b,c,d be
Element of IT holds (b,c)
'||' (a,d) & (a,b)
'||' (c,d) & (a,c)
'||' (b,d) implies (a,b)
'||' (a,c)) & for a,b,c,p,q,r be
Element of IT holds not (a,p)
'||' (a,b) & not (a,p)
'||' (a,c) & (a,p)
'||' (b,q) & (a,p)
'||' (c,r) & (a,b)
'||' (p,q) & (a,c)
'||' (p,r) implies (b,c)
'||' (q,r);
end
registration
cluster
strict
FanodesSp-like for
ParSp;
existence
proof
set FF = the
Fanoian
Field;
reconsider FdSp = (
MPS FF) as
ParSp by
Th1;
((
1_ FF)
+ (
1_ FF))
<> (
0. FF) by
VECTSP_1:def 19;
then
A1: for a,b,c,d be
Element of FdSp holds (b,c)
'||' (a,d) & (a,b)
'||' (c,d) & (a,c)
'||' (b,d) implies (a,b)
'||' (a,c) by
Th7;
(ex a,b,c be
Element of FdSp st not (a,b)
'||' (a,c)) & for a,b,c,p,q,r be
Element of FdSp holds not (a,p)
'||' (a,b) & not (a,p)
'||' (a,c) & (a,p)
'||' (b,q) & (a,p)
'||' (c,r) & (a,b)
'||' (p,q) & (a,c)
'||' (p,r) implies (b,c)
'||' (q,r) by
Th6,
Th8;
then FdSp is
FanodesSp-like by
A1;
hence thesis;
end;
end
definition
mode
FanodesSp is
FanodesSp-like
ParSp;
end
reserve FdSp for
FanodesSp;
reserve a,b,c,d,p,q,r,s,o,x,y for
Element of FdSp;
theorem ::
PARSP_2:9
Th9: p
<> q implies ex r st not (p,q)
'||' (p,r)
proof
consider a, b, c such that
A1: not (a,b)
'||' (a,c) by
Def1;
assume p
<> q;
then not (p,q)
'||' (p,a) or not (p,q)
'||' (p,b) or not (p,q)
'||' (p,c) by
A1,
PARSP_1: 38;
hence thesis;
end;
definition
let FdSp, a, b, c;
::
PARSP_2:def2
pred a,b,c
are_collinear means (a,b)
'||' (a,c);
end
theorem ::
PARSP_2:10
Th10: (a,b,c)
are_collinear implies (a,c,b)
are_collinear & (c,b,a)
are_collinear & (b,a,c)
are_collinear & (b,c,a)
are_collinear & (c,a,b)
are_collinear by
PARSP_1: 24;
theorem ::
PARSP_2:11
Th11: not (a,b,c)
are_collinear & (a,b)
'||' (p,q) & (a,c)
'||' (p,r) & p
<> q & p
<> r implies not (p,q,r)
are_collinear by
PARSP_1: 30;
theorem ::
PARSP_2:12
Th12: a
= b or b
= c or c
= a implies (a,b,c)
are_collinear by
PARSP_1: 25;
theorem ::
PARSP_2:13
Th13: a
<> b & (a,b,p)
are_collinear & (a,b,q)
are_collinear & (a,b,r)
are_collinear implies (p,q,r)
are_collinear
proof
assume that
A1: a
<> b and
A2: (a,b,p)
are_collinear and
A3: (a,b,q)
are_collinear and
A4: (a,b,r)
are_collinear ;
A5: (a,b)
'||' (a,p) by
A2;
(a,b)
'||' (a,r) by
A4;
then
A6: (a,b)
'||' (p,r) by
A5,
PARSP_1: 35;
(a,b)
'||' (a,q) by
A3;
then (a,b)
'||' (p,q) by
A5,
PARSP_1: 35;
then (p,q)
'||' (p,r) by
A1,
A6,
PARSP_1:def 12;
hence thesis;
end;
theorem ::
PARSP_2:14
Th14: p
<> q implies ex r st not (p,q,r)
are_collinear
proof
assume p
<> q;
then
consider r such that
A1: not (p,q)
'||' (p,r) by
Th9;
not (p,q,r)
are_collinear by
A1;
hence thesis;
end;
theorem ::
PARSP_2:15
Th15: (a,b,c)
are_collinear & (a,b,d)
are_collinear implies (a,b)
'||' (c,d) by
PARSP_1: 35;
theorem ::
PARSP_2:16
Th16: not (a,b,c)
are_collinear & (a,b)
'||' (c,d) implies not (a,b,d)
are_collinear
proof
assume that
A1: not (a,b,c)
are_collinear and
A2: (a,b)
'||' (c,d);
A3:
now
assume that
A4: c
<> d and
A5: a
<> d;
(a,c)
'||' (c,a) & c
<> a by
A1,
PARSP_1: 25;
then not (c,d,a)
are_collinear by
A1,
A2,
A4,
Th11;
then
A6: not (d,c,a)
are_collinear by
Th10;
A7: (d,a)
'||' (a,d) by
PARSP_1: 25;
a
<> b & (d,c)
'||' (a,b) by
A1,
A2,
Th12,
PARSP_1: 23;
hence thesis by
A5,
A6,
A7,
Th11;
end;
a
<> d by
A1,
A2,
PARSP_1: 23;
hence thesis by
A1,
A3;
end;
theorem ::
PARSP_2:17
Th17: not (a,b,c)
are_collinear & (a,b)
'||' (c,d) & c
<> d implies not (a,b,x)
are_collinear or not (c,d,x)
are_collinear by
Th16,
PARSP_1: 26;
theorem ::
PARSP_2:18
not (o,a,b)
are_collinear implies not (o,a,x)
are_collinear or not (o,b,x)
are_collinear or o
= x
proof
assume
A1: not (o,a,b)
are_collinear ;
now
assume that
A2: (o,a,x)
are_collinear and
A3: (o,b,x)
are_collinear ;
(a,o,x)
are_collinear by
A2,
Th10;
then
A4: (a,o)
'||' (a,x);
(b,o,x)
are_collinear by
A3,
Th10;
then
A5: (b,o)
'||' (b,x);
not (a,b,o)
are_collinear by
A1,
Th10;
then not (a,b)
'||' (a,o);
hence thesis by
A4,
A5,
PARSP_1: 33;
end;
hence thesis;
end;
theorem ::
PARSP_2:19
o
<> a & o
<> b & (o,a,b)
are_collinear & (o,a,p)
are_collinear & (o,b,q)
are_collinear implies (a,b)
'||' (p,q)
proof
assume that
A1: o
<> a and
A2: o
<> b and
A3: (o,a,b)
are_collinear and
A4: (o,a,p)
are_collinear and
A5: (o,b,q)
are_collinear ;
A6:
now
A7: (o,a)
'||' (o,b) by
A3;
(o,a)
'||' (o,p) by
A4;
then
A8: (o,b)
'||' (o,p) by
A1,
A7,
PARSP_1:def 12;
(o,b)
'||' (o,q) by
A5;
then (o,p)
'||' (o,q) by
A2,
A8,
PARSP_1:def 12;
then
A9: (o,p)
'||' (p,q) by
PARSP_1: 24;
(o,b)
'||' (a,b) by
A7,
PARSP_1: 24;
then
A10: (a,b)
'||' (o,p) by
A2,
A8,
PARSP_1:def 12;
assume o
<> p;
hence thesis by
A10,
A9,
PARSP_1: 26;
end;
now
assume
A11: o
= p;
then (p,a)
'||' (p,b) by
A3;
then
A12: (a,b)
'||' (p,b) by
PARSP_1: 24;
(p,b)
'||' (p,q) by
A5,
A11;
hence thesis by
A2,
A11,
A12,
PARSP_1: 26;
end;
hence thesis by
A6;
end;
theorem ::
PARSP_2:20
not (a,b)
'||' (c,d) & (a,b,p)
are_collinear & (a,b,q)
are_collinear & (c,d,p)
are_collinear & (c,d,q)
are_collinear implies p
= q
proof
assume that
A1: not (a,b)
'||' (c,d) and
A2: (a,b,p)
are_collinear & (a,b,q)
are_collinear and
A3: (c,d,p)
are_collinear & (c,d,q)
are_collinear ;
(c,d)
'||' (p,q) by
A3,
Th15;
then
A4: (p,q)
'||' (c,d) by
PARSP_1: 23;
(a,b)
'||' (p,q) by
A2,
Th15;
then (p,q)
'||' (a,b) by
PARSP_1: 23;
hence thesis by
A1,
A4,
PARSP_1:def 12;
end;
theorem ::
PARSP_2:21
a
<> b & (a,b,c)
are_collinear & (a,b)
'||' (c,d) implies (a,c)
'||' (b,d)
proof
assume that
A1: a
<> b and
A2: (a,b,c)
are_collinear and
A3: (a,b)
'||' (c,d);
now
A4: (a,b)
'||' (a,c) by
A2;
then (a,b)
'||' (c,b) by
PARSP_1: 24;
then (c,b)
'||' (c,d) by
A1,
A3,
PARSP_1:def 12;
then
A5: (b,c)
'||' (b,d) by
PARSP_1: 24;
assume
A6: b
<> c;
(b,c)
'||' (a,c) by
A4,
PARSP_1: 24;
hence thesis by
A6,
A5,
PARSP_1:def 12;
end;
hence thesis by
A3;
end;
theorem ::
PARSP_2:22
a
<> b & (a,b,c)
are_collinear & (a,b)
'||' (c,d) implies (c,b)
'||' (c,d)
proof
assume that
A1: a
<> b and
A2: (a,b,c)
are_collinear and
A3: (a,b)
'||' (c,d);
now
(a,b)
'||' (a,c) by
A2;
then
A4: (a,c)
'||' (c,b) & (a,c)
'||' (c,d) by
A1,
A3,
PARSP_1: 24,
PARSP_1:def 12;
assume a
<> c;
hence thesis by
A4,
PARSP_1:def 12;
end;
hence thesis by
A3;
end;
theorem ::
PARSP_2:23
not (o,a,c)
are_collinear & (o,a,b)
are_collinear & (o,c,p)
are_collinear & (o,c,q)
are_collinear & (a,c)
'||' (b,p) & (a,c)
'||' (b,q) implies p
= q by
PARSP_1: 34;
theorem ::
PARSP_2:24
a
<> b & (a,b,c)
are_collinear & (a,b,d)
are_collinear implies (a,c,d)
are_collinear by
PARSP_1:def 12;
theorem ::
PARSP_2:25
(a,b,c)
are_collinear & (a,c,d)
are_collinear & a
<> c implies (b,c,d)
are_collinear
proof
assume that
A1: (a,b,c)
are_collinear and
A2: (a,c,d)
are_collinear & a
<> c;
A3: (a,c,c)
are_collinear by
Th12;
(a,c,b)
are_collinear by
A1,
Th10;
hence thesis by
A2,
A3,
Th13;
end;
definition
let FdSp, a, b, c, d;
::
PARSP_2:def3
pred
parallelogram a,b,c,d means not (a,b,c)
are_collinear & (a,b)
'||' (c,d) & (a,c)
'||' (b,d);
end
theorem ::
PARSP_2:26
Th26:
parallelogram (a,b,c,d) implies a
<> b & b
<> c & c
<> a & a
<> d & b
<> d & c
<> d
proof
assume
A1:
parallelogram (a,b,c,d);
A2:
now
assume a
= d;
then (a,b)
'||' (c,a) by
A1;
then
A3: (a,b)
'||' (a,c) by
PARSP_1: 23;
not (a,b,c)
are_collinear by
A1;
hence contradiction by
A3;
end;
A4:
now
assume c
= d;
then (a,c)
'||' (b,c) by
A1;
then (c,a)
'||' (c,b) by
PARSP_1: 23;
then
A5: (a,b)
'||' (a,c) by
PARSP_1: 24;
not (a,b,c)
are_collinear by
A1;
hence contradiction by
A5;
end;
A6:
now
assume b
= d;
then (a,b)
'||' (c,b) by
A1;
then (b,a)
'||' (b,c) by
PARSP_1: 23;
then
A7: (a,b)
'||' (a,c) by
PARSP_1: 24;
not (a,b,c)
are_collinear by
A1;
hence contradiction by
A7;
end;
not (a,b,c)
are_collinear by
A1;
hence thesis by
A2,
A6,
A4,
Th12;
end;
theorem ::
PARSP_2:27
Th27:
parallelogram (a,b,c,d) implies not (a,b,c)
are_collinear & not (b,a,d)
are_collinear & not (c,d,a)
are_collinear & not (d,c,b)
are_collinear
proof
A1: (a,b)
'||' (b,a) & (a,c)
'||' (c,a) by
PARSP_1: 25;
assume
A2:
parallelogram (a,b,c,d);
then
A3: d
<> b by
Th26;
(a,c)
'||' (b,d) by
A2;
then
A4: (a,c)
'||' (d,b) by
PARSP_1: 23;
(a,b)
'||' (c,d) by
A2;
then
A5: (a,b)
'||' (d,c) by
PARSP_1: 23;
A6: ( not (a,b,c)
are_collinear ) & d
<> c by
A2,
Th26;
A7: (a,b)
'||' (c,d) & c
<> a by
A2,
Th26;
(a,c)
'||' (b,d) & b
<> a by
A2,
Th26;
hence thesis by
A1,
A7,
A5,
A4,
A6,
A3,
Th11;
end;
theorem ::
PARSP_2:28
Th28:
parallelogram (a,b,c,d) implies not (a,b,c)
are_collinear & not (b,a,d)
are_collinear & not (c,d,a)
are_collinear & not (d,c,b)
are_collinear & not (a,c,b)
are_collinear & not (b,a,c)
are_collinear & not (b,c,a)
are_collinear & not (c,a,b)
are_collinear & not (c,b,a)
are_collinear & not (b,d,a)
are_collinear & not (a,b,d)
are_collinear & not (a,d,b)
are_collinear & not (d,a,b)
are_collinear & not (d,b,a)
are_collinear & not (c,a,d)
are_collinear & not (a,c,d)
are_collinear & not (a,d,c)
are_collinear & not (d,a,c)
are_collinear & not (d,c,a)
are_collinear & not (d,b,c)
are_collinear & not (b,c,d)
are_collinear & not (b,d,c)
are_collinear & not (c,b,d)
are_collinear & not (c,d,b)
are_collinear
proof
assume
A1:
parallelogram (a,b,c,d);
then
A2: ( not (c,d,a)
are_collinear ) & not (d,c,b)
are_collinear by
Th27;
( not (a,b,c)
are_collinear ) & not (b,a,d)
are_collinear by
A1,
Th27;
hence thesis by
A2,
Th10;
end;
theorem ::
PARSP_2:29
Th29:
parallelogram (a,b,c,d) implies not (a,b,x)
are_collinear or not (c,d,x)
are_collinear
proof
assume
A1:
parallelogram (a,b,c,d);
then
A2: c
<> d by
Th26;
( not (a,b,c)
are_collinear ) & (a,b)
'||' (c,d) by
A1;
hence thesis by
A2,
Th17;
end;
theorem ::
PARSP_2:30
Th30:
parallelogram (a,b,c,d) implies
parallelogram (a,c,b,d) by
Th28;
theorem ::
PARSP_2:31
Th31:
parallelogram (a,b,c,d) implies
parallelogram (c,d,a,b) by
PARSP_1: 23,
Th28;
theorem ::
PARSP_2:32
Th32:
parallelogram (a,b,c,d) implies
parallelogram (b,a,d,c) by
PARSP_1: 23,
Th28;
theorem ::
PARSP_2:33
Th33:
parallelogram (a,b,c,d) implies
parallelogram (a,c,b,d) &
parallelogram (c,d,a,b) &
parallelogram (b,a,d,c) &
parallelogram (c,a,d,b) &
parallelogram (d,b,c,a) &
parallelogram (b,d,a,c) &
parallelogram (d,c,b,a)
proof
assume
A1:
parallelogram (a,b,c,d);
then
parallelogram (c,d,a,b) by
Th31;
then
A2:
parallelogram (c,a,d,b) by
Th30;
parallelogram (b,a,d,c) by
A1,
Th32;
hence thesis by
A1,
A2,
Th30,
Th31;
end;
theorem ::
PARSP_2:34
Th34: not (a,b,c)
are_collinear implies ex d st
parallelogram (a,b,c,d)
proof
consider d such that
A1: (a,b)
'||' (c,d) & (a,c)
'||' (b,d) by
PARSP_1:def 12;
assume not (a,b,c)
are_collinear ;
then
parallelogram (a,b,c,d) by
A1;
hence thesis;
end;
theorem ::
PARSP_2:35
Th35:
parallelogram (a,b,c,p) &
parallelogram (a,b,c,q) implies p
= q
proof
assume that
A1:
parallelogram (a,b,c,p) and
A2:
parallelogram (a,b,c,q);
(a,b)
'||' (c,p) by
A1;
then
A3: (b,c)
'||' (c,b) & (b,a)
'||' (c,p) by
PARSP_1: 23,
PARSP_1: 25;
(a,b)
'||' (c,q) by
A2;
then
A4: (b,a)
'||' (c,q) by
PARSP_1: 23;
(a,c)
'||' (b,p) by
A1;
then
A5: (c,a)
'||' (b,p) by
PARSP_1: 23;
(a,c)
'||' (b,q) by
A2;
then
A6: (c,a)
'||' (b,q) by
PARSP_1: 23;
not (b,c,a)
are_collinear by
A1,
Th28;
then not (b,c)
'||' (b,a);
hence thesis by
A3,
A4,
A5,
A6,
PARSP_1: 34;
end;
theorem ::
PARSP_2:36
Th36:
parallelogram (a,b,c,d) implies not (a,d)
'||' (b,c)
proof
assume
A1:
parallelogram (a,b,c,d);
then not (a,b,c)
are_collinear ;
then
A2: not (a,b)
'||' (a,c);
(a,b)
'||' (c,d) & (a,c)
'||' (b,d) by
A1;
then not (b,c)
'||' (a,d) by
A2,
Def1;
hence thesis by
PARSP_1: 19;
end;
theorem ::
PARSP_2:37
Th37:
parallelogram (a,b,c,d) implies not
parallelogram (a,b,d,c) by
Th36;
theorem ::
PARSP_2:38
Th38: a
<> b implies ex c st (a,b,c)
are_collinear & c
<> a & c
<> b
proof
assume a
<> b;
then
consider p such that
A1: not (a,b,p)
are_collinear by
Th14;
consider q such that
A2:
parallelogram (a,b,p,q) by
A1,
Th34;
not (p,q,b)
are_collinear by
A2,
Th28;
then
consider c such that
A3:
parallelogram (p,q,b,c) by
Th34;
A4: (p,q)
'||' (b,c) by
A3;
p
<> q & (a,b)
'||' (p,q) by
A2,
Th26;
then (a,b)
'||' (b,c) by
A4,
PARSP_1: 26;
then (b,a)
'||' (b,c) by
PARSP_1: 23;
then (b,a,c)
are_collinear ;
then
A5: (a,b,c)
are_collinear by
Th10;
A6: not (a,q)
'||' (b,p) by
A2,
Th36;
(p,b)
'||' (q,c) by
A3;
then
A7: a
<> c by
A6,
PARSP_1: 23;
b
<> c by
A3,
Th26;
hence thesis by
A7,
A5;
end;
theorem ::
PARSP_2:39
Th39:
parallelogram (a,p,b,q) &
parallelogram (a,p,c,r) implies (b,c)
'||' (q,r)
proof
assume that
A1:
parallelogram (a,p,b,q) and
A2:
parallelogram (a,p,c,r);
A3: (a,p)
'||' (c,r) & (a,c)
'||' (p,r) by
A2;
not (a,p,c)
are_collinear by
A2;
then
A4: not (a,p)
'||' (a,c);
not (a,p,b)
are_collinear by
A1;
then
A5: not (a,p)
'||' (a,b);
(a,p)
'||' (b,q) & (a,b)
'||' (p,q) by
A1;
hence thesis by
A5,
A4,
A3,
Def1;
end;
theorem ::
PARSP_2:40
Th40: not (b,q,c)
are_collinear &
parallelogram (a,p,b,q) &
parallelogram (a,p,c,r) implies
parallelogram (b,q,c,r)
proof
assume that
A1: not (b,q,c)
are_collinear and
A2:
parallelogram (a,p,b,q) and
A3:
parallelogram (a,p,c,r);
A4: (a,p)
'||' (c,r) by
A3;
a
<> p & (a,p)
'||' (b,q) by
A2,
Th26;
then
A5: (b,q)
'||' (c,r) by
A4,
PARSP_1:def 12;
(b,c)
'||' (q,r) by
A2,
A3,
Th39;
hence thesis by
A1,
A5;
end;
theorem ::
PARSP_2:41
Th41: (a,b,c)
are_collinear & b
<> c &
parallelogram (a,p,b,q) &
parallelogram (a,p,c,r) implies
parallelogram (b,q,c,r)
proof
assume that
A1: (a,b,c)
are_collinear and
A2: b
<> c and
A3:
parallelogram (a,p,b,q) and
A4:
parallelogram (a,p,c,r);
A5: b
<> q by
A3,
Th26;
(a,b)
'||' (a,c) by
A1;
then
A6: (a,b)
'||' (b,c) by
PARSP_1: 24;
thus thesis by
A2,
A3,
A4,
A5,
A6,
Th11,
Th40;
end;
theorem ::
PARSP_2:42
Th42:
parallelogram (a,p,b,q) &
parallelogram (a,p,c,r) &
parallelogram (b,q,d,s) implies (c,d)
'||' (r,s)
proof
assume that
A1:
parallelogram (a,p,b,q) and
A2:
parallelogram (a,p,c,r) and
A3:
parallelogram (b,q,d,s);
A4:
now
assume
A5: not (a,p,d)
are_collinear ;
parallelogram (b,q,a,p) by
A1,
Th33;
then
parallelogram (a,p,d,s) by
A3,
A5,
Th40;
hence thesis by
A2,
Th39;
end;
A6:
now
A7: a
<> p by
A1,
Th26;
A8: ( not (a,p,b)
are_collinear ) & (a,p)
'||' (a,p) by
A1,
PARSP_1: 25;
assume that
A9: (b,q,c)
are_collinear and
A10: (a,p,d)
are_collinear ;
a
<> b by
A1,
Th26;
then
consider x such that
A11: (a,b,x)
are_collinear and
A12: x
<> a and
A13: x
<> b by
Th38;
(a,b)
'||' (a,x) by
A11;
then
consider y such that
A14:
parallelogram (a,p,x,y) by
A12,
A8,
A7,
Th11,
Th34;
A15: not (x,y,d)
are_collinear by
A10,
A14,
Th29;
parallelogram (b,q,x,y) by
A1,
A11,
A13,
A14,
Th41;
then
A16:
parallelogram (x,y,d,s) by
A3,
A15,
Th40;
not (x,y,c)
are_collinear by
A1,
A9,
A11,
A13,
A14,
Th29,
Th41;
then
parallelogram (x,y,c,r) by
A2,
A14,
Th40;
hence thesis by
A16,
Th39;
end;
now
assume not (b,q,c)
are_collinear ;
then
parallelogram (b,q,c,r) by
A1,
A2,
Th40;
hence thesis by
A3,
Th39;
end;
hence thesis by
A4,
A6;
end;
theorem ::
PARSP_2:43
Th43: a
<> b implies ex c, d st
parallelogram (a,b,c,d)
proof
assume a
<> b;
then
consider c such that
A1: not (a,b,c)
are_collinear by
Th14;
ex d st
parallelogram (a,b,c,d) by
A1,
Th34;
hence thesis;
end;
theorem ::
PARSP_2:44
a
<> d implies ex b, c st
parallelogram (a,b,c,d)
proof
assume a
<> d;
then
consider b such that
A1: not (a,d,b)
are_collinear by
Th14;
not (b,a,d)
are_collinear by
A1,
Th10;
then
consider c such that
A2:
parallelogram (b,a,d,c) by
Th34;
parallelogram (a,b,c,d) by
A2,
Th33;
hence thesis;
end;
definition
let FdSp, a, b, r, s;
::
PARSP_2:def4
pred a,b
congr r,s means a
= b & r
= s or ex p, q st
parallelogram (p,q,a,b) &
parallelogram (p,q,r,s);
end
theorem ::
PARSP_2:45
Th45: (a,a)
congr (b,c) implies b
= c by
Th26;
theorem ::
PARSP_2:46
(a,b)
congr (c,c) implies a
= b by
Th26;
theorem ::
PARSP_2:47
(a,b)
congr (b,a) implies a
= b by
Th37;
theorem ::
PARSP_2:48
Th48: (a,b)
congr (c,d) implies (a,b)
'||' (c,d)
proof
assume
A1: (a,b)
congr (c,d);
now
assume a
<> b;
then
consider p, q such that
A2:
parallelogram (p,q,a,b) and
A3:
parallelogram (p,q,c,d) by
A1;
A4: (p,q)
'||' (c,d) by
A3;
p
<> q & (p,q)
'||' (a,b) by
A2,
Th26;
hence thesis by
A4,
PARSP_1:def 12;
end;
hence thesis by
PARSP_1: 20;
end;
theorem ::
PARSP_2:49
Th49: (a,b)
congr (c,d) implies (a,c)
'||' (b,d)
proof
assume
A1: (a,b)
congr (c,d);
A2:
now
assume
A3: a
= b;
then c
= d by
A1,
Th45;
hence thesis by
A3,
PARSP_1: 25;
end;
a
<> b implies thesis by
A1,
Th39;
hence thesis by
A2;
end;
theorem ::
PARSP_2:50
Th50: (a,b)
congr (c,d) & not (a,b,c)
are_collinear implies
parallelogram (a,b,c,d) by
Th48,
Th49;
theorem ::
PARSP_2:51
Th51:
parallelogram (a,b,c,d) implies (a,b)
congr (c,d)
proof
A1: (a,b)
'||' (a,b) by
PARSP_1: 25;
assume
A2:
parallelogram (a,b,c,d);
then
A3: ( not (a,c,b)
are_collinear ) & a
<> b by
Th26,
Th28;
a
<> c by
A2,
Th26;
then
consider p such that
A4: (a,c,p)
are_collinear and
A5: a
<> p and
A6: c
<> p by
Th38;
(a,c)
'||' (a,p) by
A4;
then
consider q such that
A7:
parallelogram (a,p,b,q) by
A5,
A1,
A3,
Th11,
Th34;
parallelogram (a,b,p,q) by
A7,
Th33;
then
parallelogram (c,d,p,q) by
A2,
A4,
A6,
Th41;
then
A8:
parallelogram (p,q,c,d) by
Th33;
parallelogram (p,q,a,b) by
A7,
Th33;
hence thesis by
A8;
end;
theorem ::
PARSP_2:52
Th52: (a,b)
congr (c,d) & (a,b,c)
are_collinear &
parallelogram (r,s,a,b) implies
parallelogram (r,s,c,d)
proof
assume that
A1: (a,b)
congr (c,d) and
A2: (a,b,c)
are_collinear and
A3:
parallelogram (r,s,a,b);
now
assume
A4: a
<> b;
then
consider p, q such that
A5:
parallelogram (p,q,a,b) and
A6:
parallelogram (p,q,c,d) by
A1;
(r,s)
'||' (a,b) & (a,b)
'||' (c,d) by
A1,
A3,
Th48;
then
A7: (r,s)
'||' (c,d) by
A4,
PARSP_1: 26;
A8:
parallelogram (a,b,r,s) by
A3,
Th33;
parallelogram (a,b,p,q) by
A5,
Th33;
then
A9: (r,c)
'||' (s,d) by
A6,
A8,
Th42;
not (r,s,c)
are_collinear by
A2,
A3,
Th29;
hence thesis by
A7,
A9;
end;
hence thesis by
A3,
Th26;
end;
theorem ::
PARSP_2:53
(a,b)
congr (c,x) & (a,b)
congr (c,y) implies x
= y
proof
assume that
A1: (a,b)
congr (c,x) and
A2: (a,b)
congr (c,y);
A3:
now
assume that a
<> b and
A4: not (a,b,c)
are_collinear ;
parallelogram (a,b,c,x) &
parallelogram (a,b,c,y) by
A1,
A2,
A4,
Th50;
hence thesis by
Th35;
end;
A5:
now
assume that
A6: a
<> b and
A7: (a,b,c)
are_collinear ;
consider p, q such that
A8:
parallelogram (a,b,p,q) by
A6,
Th43;
parallelogram (p,q,a,b) by
A8,
Th33;
then
parallelogram (p,q,c,x) &
parallelogram (p,q,c,y) by
A1,
A2,
A7,
Th52;
hence thesis by
Th35;
end;
now
assume
A9: a
= b;
then c
= x by
A1,
Th45;
hence thesis by
A2,
A9,
Th45;
end;
hence thesis by
A5,
A3;
end;
theorem ::
PARSP_2:54
ex d st (a,b)
congr (c,d)
proof
A1:
now
assume a
= b;
then (a,b)
congr (c,c);
hence thesis;
end;
A2:
now
assume that
A3: a
<> b and
A4: (a,b,c)
are_collinear ;
consider p, q such that
A5:
parallelogram (a,b,p,q) by
A3,
Th43;
not (p,q,c)
are_collinear by
A4,
A5,
Th29;
then
consider d such that
A6:
parallelogram (p,q,c,d) by
Th34;
parallelogram (p,q,a,b) by
A5,
Th33;
then (a,b)
congr (c,d) by
A6;
hence thesis;
end;
now
assume that a
<> b and
A7: not (a,b,c)
are_collinear ;
ex d st
parallelogram (a,b,c,d) by
A7,
Th34;
hence thesis by
Th51;
end;
hence thesis by
A1,
A2;
end;
theorem ::
PARSP_2:55
(a,b)
congr (a,b)
proof
now
assume a
<> b;
then
consider p, q such that
A1:
parallelogram (a,b,p,q) by
Th43;
parallelogram (p,q,a,b) by
A1,
Th33;
hence thesis;
end;
hence thesis;
end;
theorem ::
PARSP_2:56
(r,s)
congr (a,b) & (r,s)
congr (c,d) implies (a,b)
congr (c,d)
proof
assume that
A1: (r,s)
congr (a,b) and
A2: (r,s)
congr (c,d);
A3:
now
assume that r
<> s and
A4: ( not (r,s,a)
are_collinear ) & not (r,s,c)
are_collinear ;
parallelogram (r,s,a,b) &
parallelogram (r,s,c,d) by
A1,
A2,
A4,
Th50;
hence thesis;
end;
A5:
now
assume that
A6: r
<> s and
A7: (r,s,c)
are_collinear ;
consider p, q such that
A8:
parallelogram (p,q,r,s) and
A9:
parallelogram (p,q,a,b) by
A1,
A6;
parallelogram (p,q,c,d) by
A2,
A7,
A8,
Th52;
hence thesis by
A9;
end;
A10:
now
assume that
A11: r
<> s and
A12: (r,s,a)
are_collinear ;
consider p, q such that
A13:
parallelogram (p,q,r,s) and
A14:
parallelogram (p,q,c,d) by
A2,
A11;
parallelogram (p,q,a,b) by
A1,
A12,
A13,
Th52;
hence thesis by
A14;
end;
r
= s implies thesis by
A1,
A2,
Th45;
hence thesis by
A10,
A5,
A3;
end;
theorem ::
PARSP_2:57
(a,b)
congr (c,d) implies (c,d)
congr (a,b);
theorem ::
PARSP_2:58
(a,b)
congr (c,d) implies (b,a)
congr (d,c)
proof
assume
A1: (a,b)
congr (c,d);
A2:
now
assume a
<> b;
then
consider p, q such that
A3:
parallelogram (p,q,a,b) &
parallelogram (p,q,c,d) by
A1;
parallelogram (q,p,b,a) &
parallelogram (q,p,d,c) by
A3,
Th33;
hence thesis;
end;
a
= b implies thesis by
A1,
Th45;
hence thesis by
A2;
end;