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

Metamath Proof Explorer

Theorem caofdir

Description: Transfer a reverse distributive law to the function operation. (Contributed by NM, 19-Oct-2014)

Ref Expression
Hypotheses caofdi.1 
|- ( ph -> A e. V )
caofdi.2 
|- ( ph -> F : A --> K )
caofdi.3 
|- ( ph -> G : A --> S )
caofdi.4 
|- ( ph -> H : A --> S )
caofdir.5 
|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x R y ) T z ) = ( ( x T z ) O ( y T z ) ) )
Assertion caofdir 
|- ( ph -> ( ( G oF R H ) oF T F ) = ( ( G oF T F ) oF O ( H oF T F ) ) )

Proof

Step Hyp Ref Expression
1 caofdi.1 
 |-  ( ph -> A e. V )
2 caofdi.2 
 |-  ( ph -> F : A --> K )
3 caofdi.3 
 |-  ( ph -> G : A --> S )
4 caofdi.4 
 |-  ( ph -> H : A --> S )
5 caofdir.5 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x R y ) T z ) = ( ( x T z ) O ( y T z ) ) )
6 5 adantlr 
 |-  ( ( ( ph /\ w e. A ) /\ ( x e. S /\ y e. S /\ z e. K ) ) -> ( ( x R y ) T z ) = ( ( x T z ) O ( y T z ) ) )
7 3 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
8 4 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( H ` w ) e. S )
9 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. K )
10 6 7 8 9 caovdird 
 |-  ( ( ph /\ w e. A ) -> ( ( ( G ` w ) R ( H ` w ) ) T ( F ` w ) ) = ( ( ( G ` w ) T ( F ` w ) ) O ( ( H ` w ) T ( F ` w ) ) ) )
11 10 mpteq2dva 
 |-  ( ph -> ( w e. A |-> ( ( ( G ` w ) R ( H ` w ) ) T ( F ` w ) ) ) = ( w e. A |-> ( ( ( G ` w ) T ( F ` w ) ) O ( ( H ` w ) T ( F ` w ) ) ) ) )
12 ovexd 
 |-  ( ( ph /\ w e. A ) -> ( ( G ` w ) R ( H ` w ) ) e. _V )
13 3 feqmptd 
 |-  ( ph -> G = ( w e. A |-> ( G ` w ) ) )
14 4 feqmptd 
 |-  ( ph -> H = ( w e. A |-> ( H ` w ) ) )
15 1 7 8 13 14 offval2 
 |-  ( ph -> ( G oF R H ) = ( w e. A |-> ( ( G ` w ) R ( H ` w ) ) ) )
16 2 feqmptd 
 |-  ( ph -> F = ( w e. A |-> ( F ` w ) ) )
17 1 12 9 15 16 offval2 
 |-  ( ph -> ( ( G oF R H ) oF T F ) = ( w e. A |-> ( ( ( G ` w ) R ( H ` w ) ) T ( F ` w ) ) ) )
18 ovexd 
 |-  ( ( ph /\ w e. A ) -> ( ( G ` w ) T ( F ` w ) ) e. _V )
19 ovexd 
 |-  ( ( ph /\ w e. A ) -> ( ( H ` w ) T ( F ` w ) ) e. _V )
20 1 7 9 13 16 offval2 
 |-  ( ph -> ( G oF T F ) = ( w e. A |-> ( ( G ` w ) T ( F ` w ) ) ) )
21 1 8 9 14 16 offval2 
 |-  ( ph -> ( H oF T F ) = ( w e. A |-> ( ( H ` w ) T ( F ` w ) ) ) )
22 1 18 19 20 21 offval2 
 |-  ( ph -> ( ( G oF T F ) oF O ( H oF T F ) ) = ( w e. A |-> ( ( ( G ` w ) T ( F ` w ) ) O ( ( H ` w ) T ( F ` w ) ) ) ) )
23 11 17 22 3eqtr4d 
 |-  ( ph -> ( ( G oF R H ) oF T F ) = ( ( G oF T F ) oF O ( H oF T F ) ) )