caofcom

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

	Ref	Expression
Hypotheses	caofref.1	$⊢ φ \to A \in V$
	caofref.2	$⊢ φ \to F : A ⟶ S$
	caofcom.3	$⊢ φ \to G : A ⟶ S$
	caofcom.4	$⊢ (φ \land (x \in S \land y \in S)) \to x R y = y R x$
Assertion	caofcom	$⊢ φ \to F R_{f} G = G R_{f} F$

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofcom.3	$⊢ φ \to G : A ⟶ S$
4		caofcom.4	$⊢ (φ \land (x \in S \land y \in S)) \to x R y = y R x$
5	2	ffvelrnda	$⊢ (φ \land w \in A) \to F (w) \in S$
6	3	ffvelrnda	$⊢ (φ \land w \in A) \to G (w) \in S$
7	5 6	jca	$⊢ (φ \land w \in A) \to (F (w) \in S \land G (w) \in S)$
8	4	caovcomg	$⊢ (φ \land (F (w) \in S \land G (w) \in S)) \to F (w) R G (w) = G (w) R F (w)$
9	7 8	syldan	$⊢ (φ \land w \in A) \to F (w) R G (w) = G (w) R F (w)$
10	9	mpteq2dva	$⊢ φ \to (w \in A ⟼ F (w) R G (w)) = (w \in A ⟼ G (w) R F (w))$
11	2	feqmptd	$⊢ φ \to F = (w \in A ⟼ F (w))$
12	3	feqmptd	$⊢ φ \to G = (w \in A ⟼ G (w))$
13	1 5 6 11 12	offval2	$⊢ φ \to F R_{f} G = (w \in A ⟼ F (w) R G (w))$
14	1 6 5 12 11	offval2	$⊢ φ \to G R_{f} F = (w \in A ⟼ G (w) R F (w))$
15	10 13 14	3eqtr4d	$⊢ φ \to F R_{f} G = G R_{f} F$

Metamath Proof Explorer