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

Metamath Proof Explorer

Theorem caofcom

Description: Transfer a commutative 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 )
caofcom.4 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y ) = ( y R x ) )
Assertion caofcom 
|- ( ph -> ( F oF R G ) = ( G oF R F ) )

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 caofcom.4 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x R y ) = ( y R x ) )
5 2 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
6 3 ffvelcdmda 
 |-  ( ( ph /\ w e. A ) -> ( G ` w ) e. S )
7 5 6 jca 
 |-  ( ( ph /\ w e. A ) -> ( ( F ` w ) e. S /\ ( G ` w ) e. S ) )
8 4 caovcomg 
 |-  ( ( ph /\ ( ( F ` w ) e. S /\ ( G ` w ) e. S ) ) -> ( ( F ` w ) R ( G ` w ) ) = ( ( G ` w ) R ( F ` w ) ) )
9 7 8 syldan 
 |-  ( ( ph /\ w e. A ) -> ( ( F ` w ) R ( G ` w ) ) = ( ( G ` w ) R ( F ` w ) ) )
10 9 mpteq2dva 
 |-  ( ph -> ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) = ( w e. A |-> ( ( G ` w ) R ( F ` w ) ) ) )
11 2 feqmptd 
 |-  ( ph -> F = ( w e. A |-> ( F ` w ) ) )
12 3 feqmptd 
 |-  ( ph -> G = ( w e. A |-> ( G ` w ) ) )
13 1 5 6 11 12 offval2 
 |-  ( ph -> ( F oF R G ) = ( w e. A |-> ( ( F ` w ) R ( G ` w ) ) ) )
14 1 6 5 12 11 offval2 
 |-  ( ph -> ( G oF R F ) = ( w e. A |-> ( ( G ` w ) R ( F ` w ) ) ) )
15 10 13 14 3eqtr4d 
 |-  ( ph -> ( F oF R G ) = ( G oF R F ) )