Metamath Proof Explorer


Theorem tposconst

Description: The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018)

Ref Expression
Assertion tposconst tpos A × B × C = B × A × C

Proof

Step Hyp Ref Expression
1 fconstmpo A × B × C = x A , y B C
2 1 tposmpo tpos A × B × C = y B , x A C
3 fconstmpo B × A × C = y B , x A C
4 2 3 eqtr4i tpos A × B × C = B × A × C