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 ( 𝜑𝐴𝑉 )
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 𝑅 𝐹 ) )