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

Metamath Proof Explorer

Theorem caofdi

Description: Transfer a distributive law to the function operation. (Contributed by Mario Carneiro, 26-Jul-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 )
caofdi.5 
|- ( ( ph /\ ( x e. K /\ y e. S /\ z e. S ) ) -> ( x T ( y R z ) ) = ( ( x T y ) O ( x T z ) ) )
Assertion caofdi 
|- ( ph -> ( F oF T ( G oF R H ) ) = ( ( F oF T G ) oF O ( F oF T H ) ) )

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