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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝑆 )
6 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑤 ) ∈ 𝑆 )
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 𝑅 𝐹 ) )