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 ) )