This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( F e. V /\ G e. W ) -> tpos ( F oF R G ) = ( tpos F oF R tpos G ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( F e. V -> F e. _V )
2 1 adantr 
 |-  ( ( F e. V /\ G e. W ) -> F e. _V )
3 elex 
 |-  ( G e. W -> G e. _V )
4 3 adantl 
 |-  ( ( F e. V /\ G e. W ) -> G e. _V )
5 funmpt 
 |-  Fun ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } )
6 5 a1i 
 |-  ( ( F e. V /\ G e. W ) -> Fun ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
7 dftpos4 
 |-  tpos F = ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
8 tposexg 
 |-  ( F e. V -> tpos F e. _V )
9 8 adantr 
 |-  ( ( F e. V /\ G e. W ) -> tpos F e. _V )
10 7 9 eqeltrrid 
 |-  ( ( F e. V /\ G e. W ) -> ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V )
11 dftpos4 
 |-  tpos G = ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
12 tposexg 
 |-  ( G e. W -> tpos G e. _V )
13 12 adantl 
 |-  ( ( F e. V /\ G e. W ) -> tpos G e. _V )
14 11 13 eqeltrrid 
 |-  ( ( F e. V /\ G e. W ) -> ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V )
15 ofco2 
 |-  ( ( ( F e. _V /\ G e. _V ) /\ ( Fun ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) /\ ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V /\ ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) e. _V ) ) -> ( ( F oF R G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) = ( ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) oF R ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) ) )
16 2 4 6 10 14 15 syl23anc 
 |-  ( ( F e. V /\ G e. W ) -> ( ( F oF R G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) = ( ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) oF R ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) ) )
17 dftpos4 
 |-  tpos ( F oF R G ) = ( ( F oF R G ) o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
18 7 11 oveq12i 
 |-  ( tpos F oF R tpos G ) = ( ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) oF R ( G o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) ) )
19 16 17 18 3eqtr4g 
 |-  ( ( F e. V /\ G e. W ) -> tpos ( F oF R G ) = ( tpos F oF R tpos G ) )