Metamath Proof Explorer


Theorem oftpos

Description: The transposition of the value of a function operation for two functions is the value of the function operation for the two functions transposed. (Contributed by Stefan O'Rear, 17-Jul-2018)

Ref Expression
Assertion oftpos FVGWtposFRfG=tposFRftposG

Proof

Step Hyp Ref Expression
1 elex FVFV
2 1 adantr FVGWFV
3 elex GWGV
4 3 adantl FVGWGV
5 funmpt FunxV×Vx-1
6 5 a1i FVGWFunxV×Vx-1
7 dftpos4 tposF=FxV×Vx-1
8 tposexg FVtposFV
9 8 adantr FVGWtposFV
10 7 9 eqeltrrid FVGWFxV×Vx-1V
11 dftpos4 tposG=GxV×Vx-1
12 tposexg GWtposGV
13 12 adantl FVGWtposGV
14 11 13 eqeltrrid FVGWGxV×Vx-1V
15 ofco2 FVGVFunxV×Vx-1FxV×Vx-1VGxV×Vx-1VFRfGxV×Vx-1=FxV×Vx-1RfGxV×Vx-1
16 2 4 6 10 14 15 syl23anc FVGWFRfGxV×Vx-1=FxV×Vx-1RfGxV×Vx-1
17 dftpos4 tposFRfG=FRfGxV×Vx-1
18 7 11 oveq12i tposFRftposG=FxV×Vx-1RfGxV×Vx-1
19 16 17 18 3eqtr4g FVGWtposFRfG=tposFRftposG