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 ffvelrnda
 |-  ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
6 3 ffvelrnda
 |-  ( ( 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 ) )