Theorem caofcom

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

	Ref	Expression
Hypotheses	caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
	caofcom.3	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
	caofcom.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑅 𝑦 ) = ( 𝑦 𝑅 𝑥 ) )
Assertion	caofcom	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐺 ∘f 𝑅 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		caofref.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑆 )
3		caofcom.3	⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝑆 )
4		caofcom.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝑅 𝑦 ) = ( 𝑦 𝑅 𝑥 ) )
5	2	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
6	3	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
7	5 6	jca	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) )
8	4	caovcomg	⊢ ( ( 𝜑 ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 ∧ ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
9	7 8	syldan	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) = ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) )
10	9	mpteq2dva	⊢ ( 𝜑 → ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
11	2	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑤 ) ) )
12	3	feqmptd	⊢ ( 𝜑 → 𝐺 = ( 𝑤 ∈ 𝐴 ↦ ( 𝐺 ‘ 𝑤 ) ) )
13	1 5 6 11 12	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑤 ) 𝑅 ( 𝐺 ‘ 𝑤 ) ) ) )
14	1 6 5 12 11	offval2	⊢ ( 𝜑 → ( 𝐺 ∘f 𝑅 𝐹 ) = ( 𝑤 ∈ 𝐴 ↦ ( ( 𝐺 ‘ 𝑤 ) 𝑅 ( 𝐹 ‘ 𝑤 ) ) ) )
15	10 13 14	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝐺 ∘f 𝑅 𝐹 ) )