Simplify with hard to compute assumptions

Questions
,
1

Suppose we have something like this

P1 = RotationMatrix[{{1, 2, 3, 4, 2, 2, 1}, {1, 3, 4, 7, -1, -3, 10}}];
P2 = RotationMatrix[{{-1, -2, 3, 4, 3, 4, 5}, {3, 4, 
     5, -2, -1, -2, -7}}];
P3 = RotationMatrix[{{-10, 3, 3, 2, 3, 8, 5}, {10, 3, -3, 
     7, -1, -3, -2}}];
P4 = P1.P2.P3.P2;

I would like to do calculations with P4, but it is a massive and complicated matrix. I know by construction that P4 is orthonormal, but Mathematica doesn’t. Therefore evaluating

P4[[1]].P4[[2]]

takes a bit, and it is even longer to simplify it to 0. Is there a way to simplify with true assumptions that are hard computationally but known to be true? When I write

Simplify[P4[[1]].P4[[2]], P4.Transpose[P4]==IdentityMatrix[7]]

It first evaluates the assumption (which takes eternity in this case), realizes it is true and then tries to simplify the expression. I’m looking for something that can take an expression like

P4.Transpose[P4]==IdentityMatrix[7]

as a fact and use it in the simplification.

2

With incremental simplifications it becomes very fast:

P1 = RotationMatrix[{{1, 2, 3, 4, 2, 2, 1}, {1, 3, 4, 7, -1, -3, 10}}];
P2 = RotationMatrix[{{-1, -2, 3, 4, 3, 4, 5}, {3, 4, 
     5, -2, -1, -2, -7}}];
P3 = RotationMatrix[{{-10, 3, 3, 2, 3, 8, 5}, {10, 3, -3, 
     7, -1, -3, -2}}];
P4 = Simplify[Simplify[Simplify[P1 . P2] . P3] . P2];
P4[[1]] . P4[[2]] // Simplify
3

Thank you, I am aware of that. But that does not answer my question, this was just a small illustrative example. With the additional knowledge that P4 is orthonormal, this should be instant.

4

The knowledge that P4 is orthonormal simplifies itself to True. I don’t know if the algorithm can make much use of the information. I really don’t know.