let S, T be Subset of (TOP-REAL 2); :: thesis: ( S = { p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1 )) } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= - (p `1 ) } implies (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S = T )
assume A1:
( S = { p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1 )) } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= - (p `1 ) } )
; :: thesis: (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S = T
set A = 1;
set B = 0 ;
set C = 1 / 2;
set D = - (1 / 2);
set f = AffineMap 1,0 ,(1 / 2),(- (1 / 2));
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S = T
proof
thus
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S c= T
:: according to XBOOLE_0:def 10 :: thesis: T c= (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: Sproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S or x in T )
assume
x in (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S
;
:: thesis: x in T
then consider y being
set such that A2:
(
y in dom (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) &
y in S &
x = (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y )
by FUNCT_1:def 12;
consider p being
Point of
(TOP-REAL 2) such that A3:
(
y = p &
p `2 <= 1
- (2 * (p `1 )) )
by A1, A2;
set b =
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . p;
A4:
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . p = |[((1 * (p `1 )) + 0 ),(((1 / 2) * (p `2 )) + (- (1 / 2)))]|
by JGRAPH_2:def 2;
then A5:
((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . p) `1 = (1 * (p `1 )) + 0
by EUCLID:56;
(1 / 2) * (p `2 ) <= (1 / 2) * (1 - (2 * (p `1 )))
by A3, XREAL_1:66;
then
((1 / 2) * (p `2 )) + (- (1 / 2)) <= ((1 / 2) - (p `1 )) + (- (1 / 2))
by XREAL_1:8;
then
((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . p) `2 <= - (((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . p) `1 )
by A4, A5, EUCLID:56;
hence
x in T
by A1, A2, A3;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in T or x in (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S )
assume
x in T
;
:: thesis: x in (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S
then consider p being
Point of
(TOP-REAL 2) such that A6:
(
x = p &
p `2 <= - (p `1 ) )
by A1;
AffineMap 1,
0 ,
(1 / 2),
(- (1 / 2)) is
onto
by JORDAN1K:36;
then
rng (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) = the
carrier of
(TOP-REAL 2)
by FUNCT_2:def 3;
then consider y being
set such that A7:
(
y in dom (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) &
x = (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y )
by A6, FUNCT_1:def 5;
reconsider y =
y as
Point of
(TOP-REAL 2) by A7;
set b =
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y;
A8:
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y = |[((1 * (y `1 )) + 0 ),(((1 / 2) * (y `2 )) + (- (1 / 2)))]|
by JGRAPH_2:def 2;
then A9:
((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y) `1 = y `1
by EUCLID:56;
A10:
((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y) `2 = ((1 / 2) * (y `2 )) + (- (1 / 2))
by A8, EUCLID:56;
2
* (((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y) `2 ) <= 2
* (- (y `1 ))
by A6, A7, A9, XREAL_1:66;
then
(2 * (((AffineMap 1,0 ,(1 / 2),(- (1 / 2))) . y) `2 )) + 1
<= (2 * (- (y `1 ))) + 1
by XREAL_1:8;
then
y `2 <= 1
- (2 * (y `1 ))
by A10;
then
y in S
by A1;
hence
x in (AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S
by A7, FUNCT_1:def 12;
:: thesis: verum
end;
hence
(AffineMap 1,0 ,(1 / 2),(- (1 / 2))) .: S = T
; :: thesis: verum