Question: In Maple, how do I show two geometric regions (defined by some formulae) are equal?

Let us begin with few simulations: 
 

restart;

CodeTools:-Usage(plots['pointplot3d'](Matrix((proc (_) options operator, arrow; [_[() .. (), 1]-_[() .. (), 3], _[() .. (), 2]-_[() .. (), 4], _[() .. (), 5]] end proc)(convert(ssystem("wolframscript -code \"RandomPoint[Simplex[IdentityMatrix[5]], 2*^4]\"")[-1], FromMma)), scan = [rectangular, columns], datatype = float[4]), scaling = constrained))

memory used=0.57TiB, alloc change=91.51MiB, cpu time=18.77m, real time=15.86m, gc time=4.91m

 

CodeTools:-Usage(plots['pointplot3d'](Matrix((proc (_) options operator, arrow; [_[() .. (), 1]-_[() .. (), 3], _[() .. (), 2]-_[() .. (), 4], _[() .. (), 5]] end proc)(convert(ssystem("wolframscript -code \"RandomPoint[Sphere[5], 2*^4, ConstantArray[List[0, 1], 5]]\"")[-1], FromMma)), scan = columns, datatype = float[4]), scaling = constrained))

memory used=0.56TiB, alloc change=-12.08MiB, cpu time=18.70m, real time=15.11m, gc time=5.69m

 

NULL


 

Download iDistributionVector.mws

Well, I'd like to prove (through the use of Maple): 

transform((x1, x2, x3, x4, x5) -> [x1 - x3, x2 - x4, x5])(inequal(And((x || (1 .. 5)) >=~ 0, norm([x || (1 .. 5)], 1) = 1))) # not Maple syntax

is equivalent to a filled pyramid

ImplicitRegion((X, Y, Z), 0 <= Z <= 1 - abs(X) - abs(Y)) # not SymPy syntax

transform((x1, x2, x3, x4, x5) -> [x1 - x3, x2 - x4, x5])(inequal(And((x || (1 .. 5)) >=~ 0, norm([x || (1 .. 5)], 2) = 1))) # not Maple syntax

is equivalent to a hemi-ball

ImplicitRegion((X, Y, Z), 0 <= Z <= sqrt(1 - X**2 - Y**2)) # not SymPy syntax

, and 

transform((x1, x2, x3, x4, x5) -> [x1 - x3, x2 - x4, x5])(inequal(And((x || (1 .. 5)) >=~ 0, norm([x || (1 .. 5)], 'infinity') = 1))) # not Maple syntax

is equivalent to a solid cuboid

ImplicitRegion((X, Y, Z), -1 <= X <= 1 & -1 <= Y <= 1 & 0 <= Z <= 1) # not SymPy syntax

. (Here, for the convenience of the descriptions, I utilize some non-standard notation from sympy.vector.) 
Note that ”two regions are equal" is a two-way property, which means the following proof 

is(Z >= 0) and is(Z <= 1 - abs(X) - abs(Y)) assuming (X, Y, Z) =~ (x1 - x3, x2 - x4, x5), x || (1 .. 5) >=~ 0, add(x || (1 .. 5)) = 1;
                              true
(*Accordingly, the latter region is a subset of the former one.*) 

is incomplete (because it's hard to determine whether the is routine always performs equivalent transformations in internal evaluation). 

So, can I execute such eliminations in Maple?

Please Wait...