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

Metamath Proof Explorer

Theorem caofass

Description: Transfer an associative law to the function operation. (Contributed by Mario Carneiro, 26-Jul-2014)

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

Proof

Step Hyp Ref Expression
1 caofref.1 
 |-  ( ph -> A e. V )
2 caofref.2 
 |-  ( ph -> F : A --> S )
3 caofcom.3 
 |-  ( ph -> G : A --> S )
4 caofass.4 
 |-  ( ph -> H : A --> S )
5 caofass.5 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x R y ) T z ) = ( x O ( y P z ) ) )
6 5 ralrimivvva 
 |-  ( ph -> A. x e. S A. y e. S A. z e. S ( ( x R y ) T z ) = ( x O ( y P z ) ) )
7 6 adantr 
 |-  ( ( ph /\ w e. A ) -> A. x e. S A. y e. S A. z e. S ( ( x R y ) T z ) = ( x O ( y P z ) ) )
8 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
9 3 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
10 4 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( H ` w ) e. S )
11 oveq1 
 |-  ( x = ( F ` w ) -> ( x R y ) = ( ( F ` w ) R y ) )
12 11 oveq1d 
 |-  ( x = ( F ` w ) -> ( ( x R y ) T z ) = ( ( ( F ` w ) R y ) T z ) )
13 oveq1 
 |-  ( x = ( F ` w ) -> ( x O ( y P z ) ) = ( ( F ` w ) O ( y P z ) ) )
14 12 13 eqeq12d 
 |-  ( x = ( F ` w ) -> ( ( ( x R y ) T z ) = ( x O ( y P z ) ) <-> ( ( ( F ` w ) R y ) T z ) = ( ( F ` w ) O ( y P z ) ) ) )
15 oveq2 
 |-  ( y = ( G ` w ) -> ( ( F ` w ) R y ) = ( ( F ` w ) R ( G ` w ) ) )
16 15 oveq1d 
 |-  ( y = ( G ` w ) -> ( ( ( F ` w ) R y ) T z ) = ( ( ( F ` w ) R ( G ` w ) ) T z ) )
17 oveq1 
 |-  ( y = ( G ` w ) -> ( y P z ) = ( ( G ` w ) P z ) )
18 17 oveq2d 
 |-  ( y = ( G ` w ) -> ( ( F ` w ) O ( y P z ) ) = ( ( F ` w ) O ( ( G ` w ) P z ) ) )
19 16 18 eqeq12d 
 |-  ( y = ( G ` w ) -> ( ( ( ( F ` w ) R y ) T z ) = ( ( F ` w ) O ( y P z ) ) <-> ( ( ( F ` w ) R ( G ` w ) ) T z ) = ( ( F ` w ) O ( ( G ` w ) P z ) ) ) )
20 oveq2 
 |-  ( z = ( H ` w ) -> ( ( ( F ` w ) R ( G ` w ) ) T z ) = ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) )
21 oveq2 
 |-  ( z = ( H ` w ) -> ( ( G ` w ) P z ) = ( ( G ` w ) P ( H ` w ) ) )
22 21 oveq2d 
 |-  ( z = ( H ` w ) -> ( ( F ` w ) O ( ( G ` w ) P z ) ) = ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) )
23 20 22 eqeq12d 
 |-  ( z = ( H ` w ) -> ( ( ( ( F ` w ) R ( G ` w ) ) T z ) = ( ( F ` w ) O ( ( G ` w ) P z ) ) <-> ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) = ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) ) )
24 14 19 23 rspc3v 
 |-  ( ( ( F ` w ) e. S /\ ( G ` w ) e. S /\ ( H ` w ) e. S ) -> ( A. x e. S A. y e. S A. z e. S ( ( x R y ) T z ) = ( x O ( y P z ) ) -> ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) = ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) ) )
25 8 9 10 24 syl3anc 
 |-  ( ( ph /\ w e. A ) -> ( A. x e. S A. y e. S A. z e. S ( ( x R y ) T z ) = ( x O ( y P z ) ) -> ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) = ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) ) )
26 7 25 mpd 
 |-  ( ( ph /\ w e. A ) -> ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) = ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) )
27 26 mpteq2dva 
 |-  ( ph -> ( w e. A |-> ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) ) = ( w e. A |-> ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) ) )
28 ovexd 
 |-  ( ( ph /\ w e. A ) -> ( ( F ` w ) R ( G ` w ) ) e. _V )
29 2 feqmptd 
 |-  ( ph -> F = ( w e. A |-> ( F ` w ) ) )
30 3 feqmptd 
 |-  ( ph -> G = ( w e. A |-> ( G ` w ) ) )
31 1 8 9 29 30 offval2 
 |-  ( ph -> ( F oF R G ) = ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) )
32 4 feqmptd 
 |-  ( ph -> H = ( w e. A |-> ( H ` w ) ) )
33 1 28 10 31 32 offval2 
 |-  ( ph -> ( ( F oF R G ) oF T H ) = ( w e. A |-> ( ( ( F ` w ) R ( G ` w ) ) T ( H ` w ) ) ) )
34 ovexd 
 |-  ( ( ph /\ w e. A ) -> ( ( G ` w ) P ( H ` w ) ) e. _V )
35 1 9 10 30 32 offval2 
 |-  ( ph -> ( G oF P H ) = ( w e. A |-> ( ( G ` w ) P ( H ` w ) ) ) )
36 1 8 34 29 35 offval2 
 |-  ( ph -> ( F oF O ( G oF P H ) ) = ( w e. A |-> ( ( F ` w ) O ( ( G ` w ) P ( H ` w ) ) ) ) )
37 27 33 36 3eqtr4d 
 |-  ( ph -> ( ( F oF R G ) oF T H ) = ( F oF O ( G oF P H ) ) )