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.